![]() |
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 1849 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1849 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 210 df-ex 1782 |
This theorem is referenced by: 3exbii 1851 2exanali 1861 4exdistrv 1957 3exdistr 1962 cbvex4vw 2049 eeeanv 2360 ee4anv 2361 2exsb 2368 cbvex4v 2426 2sb5rf 2485 sbel2x 2487 2mo2 2709 rexcomOLD 3309 rexcomf 3311 reeanlem 3318 ceqsex3v 3493 ceqsex4v 3494 ceqsex8v 3496 copsexgw 5346 copsexg 5347 opelopabsbALT 5381 opabn0 5405 elxp2 5543 rabxp 5564 elxp3 5582 elvv 5590 elvvv 5591 copsex2gb 5643 elcnv2 5712 cnvuni 5721 xpdifid 5992 coass 6085 fununi 6399 dfmpt3 6454 tpres 6940 dfoprab2 7191 dmoprab 7234 rnoprab 7236 mpomptx 7244 resoprab 7249 elrnmpores 7267 ov3 7291 ov6g 7292 uniuni 7464 opabex3rd 7649 oprabex3 7660 wfrlem4 7941 oeeu 8212 xpassen 8594 zorn2lem6 9912 ltresr 10551 axaddf 10556 axmulf 10557 hashfun 13794 hash2prb 13826 5oalem7 29443 mpomptxf 30442 eulerpartlemgvv 31744 bnj600 32301 bnj916 32315 bnj983 32333 bnj986 32337 bnj996 32338 bnj1021 32348 dfacycgr1 32504 satfv1 32723 elima4 33132 brtxp2 33455 brpprod3a 33460 brpprod3b 33461 elfuns 33489 brcart 33506 brimg 33511 brapply 33512 brsuccf 33515 brrestrict 33523 dfrdg4 33525 ellines 33726 bj-cbvex4vv 34242 itg2addnclem3 35110 brxrn2 35787 dfxrn2 35788 ecxrn 35799 inxpxrn 35803 rnxrn 35806 dalem20 36989 dvhopellsm 38413 diblsmopel 38467 en2pr 40246 pm11.52 41091 pm11.6 41096 pm11.7 41100 opelopab4 41257 stoweidlem35 42677 fundcmpsurbijinj 43927 mpomptx2 44736 |
Copyright terms: Public domain | W3C validator |