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 3023 | . 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) |
3 | 2 | rexbii 3023 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-rex 2902 |
This theorem is referenced by: rexnal3 3026 ralnex2 3027 ralnex3 3028 3reeanv 3087 addcompr 9722 mulcompr 9724 4fvwrd4 12328 ntrivcvgmul 14473 prodmo 14505 pythagtriplem2 15360 pythagtrip 15377 isnsgrp 17111 efgrelexlemb 17986 ordthaus 20998 regr1lem2 21353 fmucndlem 21905 dfcgra2 25521 axpasch 25621 axeuclid 25643 axcontlem4 25647 frgrawopreglem5 26575 xrofsup 28923 poseq 30994 altopelaltxp 31253 brsegle 31385 mzpcompact2lem 36332 sbc4rex 36371 7rexfrabdioph 36382 expdiophlem1 36606 fourierdlem42 39042 umgr2edg1 40438 frgrwopreglem5 41485 ldepslinc 42092 |
Copyright terms: Public domain | W3C validator |