![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2rexbii | Structured version Visualization version GIF version |
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.) |
Ref | Expression |
---|---|
2rexbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2rexbii | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2rexbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | rexbii 3084 | . 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) |
3 | 2 | rexbii 3084 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-rex 3061 |
This theorem is referenced by: rexnal3 3126 3reeanv 3218 2nreu 4438 poxp2 8149 poxp3 8156 poseq 8164 1sdom 9275 ttrcltr 9752 addcompr 11055 mulcompr 11057 4fvwrd4 13669 ntrivcvgmul 15901 prodmo 15933 pythagtriplem2 16814 pythagtrip 16831 cat1 18114 isnsgrp 18711 efgrelexlemb 19744 ordthaus 23376 regr1lem2 23732 fmucndlem 24284 madeval2 27874 dfcgra2 28754 axpasch 28872 axeuclid 28894 axcontlem4 28898 umgr2edg1 29144 wwlksnwwlksnon 29846 xrofsup 32674 satfvsucsuc 35206 satf0 35213 altopelaltxp 35813 brsegle 35945 fimgmcyclem 42223 fimgmcyc 42224 mzpcompact2lem 42445 sbc4rex 42483 7rexfrabdioph 42494 expdiophlem1 42716 fourierdlem42 45806 prpair 47109 ldepslinc 47928 sepnsepolem1 48291 |
Copyright terms: Public domain | W3C validator |