![]() |
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 |
---|---|
2ralbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
2 | 1 | anassrs 468 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | rexbidva 3172 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | rexbidva 3172 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2106 ∃wrex 3072 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-rex 3073 |
This theorem is referenced by: 2reu4lem 4482 wrdl3s3 14848 bezoutlem2 16418 bezoutlem4 16420 vdwmc2 16848 lsmcom2 19433 lsmass 19447 lsmcomx 19630 lsmspsn 20541 hausdiag 22992 imasf1oxms 23841 istrkg2ld 27300 iscgra 27649 axeuclid 27810 elwwlks2 28809 elwspths2spth 28810 fusgr2wsp2nb 29176 shscom 30159 lsmssass 32078 sategoelfvb 33904 mulsval 34397 3dim0 37909 islpln5 37987 islvol5 38031 isline2 38226 isline3 38228 paddcom 38265 cdlemg2cex 39043 prprspr2 45680 pgrpgt2nabl 46412 elbigolo1 46613 |
Copyright terms: Public domain | W3C validator |