![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2exbii | Structured version Visualization version GIF version |
Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
2exbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2exbii | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2exbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | exbii 1851 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1851 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 3exbii 1853 2exanali 1864 4exdistrv 1961 3exdistr 1965 cbvex4vw 2046 eeeanv 2347 ee4anv 2348 2exsb 2357 cbvex4v 2414 2sb5rf 2471 sbel2x 2473 2mo2 2648 reeanlem 3219 rexcomf 3289 ceqsex3v 3503 ceqsex4v 3504 ceqsex8v 3506 copsexgw 5452 copsexg 5453 copsex2g 5455 vopelopabsb 5491 opabn0 5515 elxp2 5662 rabxp 5685 elxp3 5703 elvv 5711 elvvv 5712 copsex2gb 5767 elcnv2 5838 cnvuni 5847 xpdifid 6125 coass 6222 fununi 6581 dfmpt3 6640 tpres 7155 dfoprab2 7420 dmoprab 7463 rnoprab 7465 mpomptx 7474 resoprab 7479 elrnmpores 7498 ov3 7522 ov6g 7523 uniuni 7701 opabex3rd 7904 oprabex3 7915 wfrlem4OLD 8263 oeeu 8555 xpassen 9017 sbthfilem 9152 zorn2lem6 10444 ltresr 11083 axaddf 11088 axmulf 11089 hashfun 14344 hash2prb 14378 5oalem7 30644 mpomptxf 31639 eulerpartlemgvv 33016 bnj600 33571 bnj916 33585 bnj983 33603 bnj986 33607 bnj996 33608 bnj1021 33618 dfacycgr1 33778 satfv1 33997 elima4 34389 brtxp2 34495 brpprod3a 34500 brpprod3b 34501 elfuns 34529 brcart 34546 brimg 34551 brapply 34552 brsuccf 34555 brrestrict 34563 dfrdg4 34565 ellines 34766 bj-cbvex4vv 35299 itg2addnclem3 36160 brxrn2 36866 dfxrn2 36867 ecxrn 36878 inxpxrn 36886 rnxrn 36889 dalem20 38185 dvhopellsm 39609 diblsmopel 39663 ralopabb 41757 en2pr 41893 pm11.52 42741 pm11.6 42746 pm11.7 42750 opelopab4 42907 stoweidlem35 44350 fundcmpsurbijinj 45676 mpomptx2 46484 |
Copyright terms: Public domain | W3C validator |