![]() |
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 1843 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1843 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∃wex 1774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-ex 1775 |
This theorem is referenced by: 3exbii 1845 2exanali 1856 4exdistrv 1953 3exdistr 1957 cbvex4vw 2038 eeeanv 2341 ee4anv 2342 2exsb 2351 cbvex4v 2409 2sb5rf 2466 sbel2x 2468 2mo2 2636 reeanlem 3216 rexcomf 3291 cgsex4g 3511 ceqsex3v 3523 ceqsex4v 3524 ceqsex8v 3526 copsexgw 5496 copsexg 5497 copsex2g 5499 vopelopabsb 5535 opabn0 5559 elxp2 5706 rabxp 5730 elxp3 5748 elvv 5756 elvvv 5757 copsex2gb 5812 elcnv2 5884 cnvuni 5893 cnvopab 6149 xpdifid 6179 coass 6276 fununi 6634 dfmpt3 6695 tpres 7218 dfoprab2 7483 dmoprab 7527 rnoprab 7529 mpomptx 7538 resoprab 7543 elrnmpores 7564 ov3 7589 ov6g 7590 uniuni 7770 opabex3rd 7980 oprabex3 7991 wfrlem4OLD 8342 oeeu 8633 xpassen 9104 sbthfilem 9235 zorn2lem6 10544 ltresr 11183 axaddf 11188 axmulf 11189 hashfun 14454 hash2prb 14491 5oalem7 31593 mpomptxf 32595 eulerpartlemgvv 34210 bnj600 34764 bnj916 34778 bnj983 34796 bnj986 34800 bnj996 34801 bnj1021 34811 dfacycgr1 34972 satfv1 35191 elima4 35599 brtxp2 35705 brpprod3a 35710 brpprod3b 35711 elfuns 35739 brcart 35756 brimg 35761 brapply 35762 brsuccf 35765 brrestrict 35773 dfrdg4 35775 ellines 35976 bj-cbvex4vv 36510 itg2addnclem3 37374 brxrn2 38073 dfxrn2 38074 ecxrn 38085 inxpxrn 38093 rnxrn 38096 dalem20 39392 dvhopellsm 40816 diblsmopel 40870 ralopabb 43078 en2pr 43214 pm11.52 44061 pm11.6 44066 pm11.7 44070 opelopab4 44227 stoweidlem35 45656 fundcmpsurbijinj 46982 mpomptx2 47713 |
Copyright terms: Public domain | W3C validator |