|   | 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 1847 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) | 
| 3 | 2 | exbii 1847 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 | 
| This theorem is referenced by: 3exbii 1849 2exanali 1859 4exdistrv 1955 3exdistr 1959 cbvex4vw 2040 eeeanv 2351 ee4anv 2352 ee4anvOLD 2353 2exsb 2362 cbvex4v 2419 2sb5rf 2476 sbel2x 2478 2mo2 2646 r3ex 3197 reeanlem 3227 rexcomf 3302 cgsex4g 3527 ceqsex3v 3536 ceqsex4v 3537 ceqsex8v 3539 copsexgw 5494 copsexg 5495 copsex2g 5497 vopelopabsb 5533 opabn0 5557 elxp2 5708 rabxp 5732 elxp3 5750 elvv 5759 elvvv 5760 copsex2gb 5815 elcnv2 5887 cnvuni 5896 cnvopab 6156 xpdifid 6187 coass 6284 fununi 6640 dfmpt3 6701 tpres 7222 dfoprab2 7492 cbvoprab3v 7526 dmoprab 7537 rnoprab 7539 mpomptx 7547 resoprab 7552 elrnmpores 7572 ov3 7597 ov6g 7598 uniuni 7783 opabex3rd 7992 oprabex3 8003 wfrlem4OLD 8353 oeeu 8642 xpassen 9107 sbthfilem 9239 zorn2lem6 10542 ltresr 11181 axaddf 11186 axmulf 11187 hashfun 14477 hash2prb 14512 5oalem7 31680 mpomptxf 32688 eulerpartlemgvv 34379 bnj600 34934 bnj916 34948 bnj983 34966 bnj986 34970 bnj996 34971 bnj1021 34981 dfacycgr1 35150 satfv1 35369 elima4 35777 brtxp2 35883 brpprod3a 35888 brpprod3b 35889 elfuns 35917 brcart 35934 brimg 35939 brapply 35940 brsuccf 35943 brrestrict 35951 dfrdg4 35953 ellines 36154 bj-cbvex4vv 36807 itg2addnclem3 37681 brxrn2 38377 dfxrn2 38378 ecxrn 38389 inxpxrn 38397 rnxrn 38400 dalem20 39696 dvhopellsm 41120 diblsmopel 41174 ralopabb 43429 en2pr 43565 pm11.52 44411 pm11.6 44416 pm11.7 44420 opelopab4 44576 stoweidlem35 46055 fundcmpsurbijinj 47402 mpomptx2 48256 | 
| Copyright terms: Public domain | W3C validator |