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 1855 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1855 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∃wex 1787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-ex 1788 |
This theorem is referenced by: 3exbii 1857 2exanali 1868 4exdistrv 1965 3exdistr 1969 cbvex4vw 2050 eeeanv 2351 ee4anv 2352 2exsb 2359 cbvex4v 2414 2sb5rf 2471 sbel2x 2473 2mo2 2648 rexcomf 3267 reeanlem 3274 ceqsex3v 3457 ceqsex4v 3458 ceqsex8v 3460 copsexgw 5370 copsexg 5371 copsex2g 5373 vopelopabsb 5407 opabn0 5431 elxp2 5572 rabxp 5594 elxp3 5612 elvv 5620 elvvv 5621 copsex2gb 5673 elcnv2 5743 cnvuni 5752 xpdifid 6028 coass 6126 fununi 6452 dfmpt3 6509 tpres 7013 dfoprab2 7266 dmoprab 7309 rnoprab 7311 mpomptx 7320 resoprab 7325 elrnmpores 7344 ov3 7368 ov6g 7369 uniuni 7544 opabex3rd 7736 oprabex3 7747 wfrlem4 8055 oeeu 8328 xpassen 8736 zorn2lem6 10112 ltresr 10751 axaddf 10756 axmulf 10757 hashfun 14001 hash2prb 14035 5oalem7 29738 mpomptxf 30733 eulerpartlemgvv 32052 bnj600 32609 bnj916 32623 bnj983 32641 bnj986 32645 bnj996 32646 bnj1021 32656 dfacycgr1 32816 satfv1 33035 elima4 33466 brtxp2 33917 brpprod3a 33922 brpprod3b 33923 elfuns 33951 brcart 33968 brimg 33973 brapply 33974 brsuccf 33977 brrestrict 33985 dfrdg4 33987 ellines 34188 bj-cbvex4vv 34721 itg2addnclem3 35565 brxrn2 36240 dfxrn2 36241 ecxrn 36252 inxpxrn 36256 rnxrn 36259 dalem20 37442 dvhopellsm 38866 diblsmopel 38920 en2pr 40828 pm11.52 41676 pm11.6 41681 pm11.7 41685 opelopab4 41842 stoweidlem35 43249 fundcmpsurbijinj 44533 mpomptx2 45341 |
Copyright terms: Public domain | W3C validator |