![]() |
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 |
---|---|
rexbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2rexbii | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | rexbii 3188 | . 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) |
3 | 2 | rexbii 3188 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∃wrex 3083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-rex 3088 |
This theorem is referenced by: rexnal3 3199 ralnex2OLD 3201 ralnex3OLD 3203 3reeanv 3303 2nreu 4270 addcompr 10233 mulcompr 10235 4fvwrd4 12836 ntrivcvgmul 15108 prodmo 15140 pythagtriplem2 16000 pythagtrip 16017 isnsgrp 17746 efgrelexlemb 18626 ordthaus 21686 regr1lem2 22042 fmucndlem 22593 dfcgra2 26308 axpasch 26420 axeuclid 26442 axcontlem4 26446 umgr2edg1 26686 wwlksnwwlksnon 27411 xrofsup 30233 poseq 32556 madeval2 32751 altopelaltxp 32898 brsegle 33030 mzpcompact2lem 38688 sbc4rex 38727 7rexfrabdioph 38738 expdiophlem1 38959 fourierdlem42 41811 prpair 42971 ldepslinc 43871 |
Copyright terms: Public domain | W3C validator |