Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2rexbidva | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.) |
Ref | Expression |
---|---|
2rexbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2rexbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
2 | 1 | anassrs 680 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | rexbidva 3049 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | rexbidva 3049 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∈ wcel 1990 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-rex 2918 |
This theorem is referenced by: wrdl3s3 13705 bezoutlem2 15257 bezoutlem4 15259 vdwmc2 15683 lsmcom2 18070 lsmass 18083 lsmcomx 18259 lsmspsn 19084 hausdiag 21448 imasf1oxms 22294 istrkg2ld 25359 iscgra 25701 axeuclid 25843 wwlksnwwlksnon 26810 wspthsnwspthsnon 26811 elwwlks2 26861 elwspths2spth 26862 fusgr2wsp2nb 27198 shscom 28178 3dim0 34743 islpln5 34821 islvol5 34865 isline2 35060 isline3 35062 paddcom 35099 cdlemg2cex 35879 2reu4a 41189 pgrpgt2nabl 42147 elbigolo1 42351 |
Copyright terms: Public domain | W3C validator |