![]() |
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 469 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | rexbidva 3170 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | rexbidva 3170 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-rex 3071 |
This theorem is referenced by: 2reu4lem 4484 wrdl3s3 14857 bezoutlem2 16426 bezoutlem4 16428 vdwmc2 16856 lsmcom2 19442 lsmass 19456 lsmcomx 19639 lsmspsn 20560 hausdiag 23012 imasf1oxms 23861 mulsval 27396 istrkg2ld 27444 iscgra 27793 axeuclid 27954 elwwlks2 28953 elwspths2spth 28954 fusgr2wsp2nb 29320 shscom 30303 lsmssass 32231 sategoelfvb 34070 3dim0 37966 islpln5 38044 islvol5 38088 isline2 38283 isline3 38285 paddcom 38322 cdlemg2cex 39100 prprspr2 45796 pgrpgt2nabl 46528 elbigolo1 46729 |
Copyright terms: Public domain | W3C validator |