| 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 3094 | . 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) |
| 3 | 2 | rexbii 3094 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: rexnal3 3136 3reeanv 3230 2nreu 4444 poxp2 8168 poxp3 8175 poseq 8183 1sdom 9284 ttrcltr 9756 addcompr 11061 mulcompr 11063 4fvwrd4 13688 ntrivcvgmul 15938 prodmo 15972 pythagtriplem2 16855 pythagtrip 16872 cat1 18142 isnsgrp 18736 efgrelexlemb 19768 ordthaus 23392 regr1lem2 23748 fmucndlem 24300 madeval2 27892 zaddscl 28380 zmulscld 28383 dfcgra2 28838 axpasch 28956 axeuclid 28978 axcontlem4 28982 umgr2edg1 29228 wwlksnwwlksnon 29935 xrofsup 32771 satfvsucsuc 35370 satf0 35377 altopelaltxp 35977 brsegle 36109 fimgmcyclem 42543 fimgmcyc 42544 mzpcompact2lem 42762 sbc4rex 42800 7rexfrabdioph 42811 expdiophlem1 43033 fourierdlem42 46164 prpair 47488 ldepslinc 48426 sepnsepolem1 48819 |
| Copyright terms: Public domain | W3C validator |