![]() |
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 form). (Contributed by NM, 15-Dec-2004.) |
Ref | Expression |
---|---|
2rexbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2rexbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
2 | 1 | anassrs 468 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | rexbidva 3261 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | rexbidva 3261 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2083 ∃wrex 3108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1766 df-rex 3113 |
This theorem is referenced by: 2reu4lem 4385 wrdl3s3 14164 bezoutlem2 15721 bezoutlem4 15723 vdwmc2 16148 lsmcom2 18514 lsmass 18527 lsmcomx 18703 lsmspsn 19550 hausdiag 21941 imasf1oxms 22786 istrkg2ld 25932 iscgra 26281 axeuclid 26436 elwwlks2 27431 elwspths2spth 27432 fusgr2wsp2nb 27801 shscom 28783 sategoelfvb 32276 3dim0 36145 islpln5 36223 islvol5 36267 isline2 36462 isline3 36464 paddcom 36501 cdlemg2cex 37279 prprspr2 43184 pgrpgt2nabl 43916 elbigolo1 44120 |
Copyright terms: Public domain | W3C validator |