![]() |
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 1947 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1947 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∃wex 1878 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 |
This theorem depends on definitions: df-bi 199 df-ex 1879 |
This theorem is referenced by: 3exbii 1949 4exdistrv 2055 3exdistr 2059 eeeanv 2374 ee4anv 2375 2exsb 2383 cbvex4v 2435 2sb5rf 2585 sbel2x 2592 2mo2 2730 rexcomf 3307 reean 3316 ceqsex3v 3463 ceqsex4v 3464 ceqsex8v 3466 vtocl3 3478 copsexg 5178 opelopabsbALT 5212 opabn0 5234 elxp2 5370 rabxp 5391 elxp3 5406 elvv 5414 elvvv 5415 copsex2gb 5468 elcnv2 5536 cnvuni 5545 xpdifid 5807 coass 5899 fununi 6201 dfmpt3 6251 tpres 6727 dfoprab2 6966 dmoprab 7006 rnoprab 7008 mpt2mptx 7016 resoprab 7021 elrnmpt2res 7039 ov3 7062 ov6g 7063 uniuni 7236 oprabex3 7422 wfrlem4 7688 wfrlem4OLD 7689 oeeu 7955 xpassen 8329 zorn2lem6 9645 ltresr 10284 axaddf 10289 axmulf 10290 hashfun 13520 hash2prb 13550 5oalem7 29070 mpt2mptxf 30021 eulerpartlemgvv 30979 bnj600 31531 bnj916 31545 bnj983 31563 bnj986 31566 bnj996 31567 bnj1021 31576 elima4 32212 brtxp2 32522 brpprod3a 32527 brpprod3b 32528 elfuns 32556 brcart 32573 brimg 32578 brapply 32579 brsuccf 32582 brrestrict 32590 dfrdg4 32592 ellines 32793 bj-cbvex4vv 33273 cnfinltrel 33781 itg2addnclem3 34001 brxrn2 34680 dfxrn2 34681 ecxrn 34692 inxpxrn 34696 rnxrn 34699 dalem20 35763 dvhopellsm 37187 diblsmopel 37241 pm11.52 39421 2exanali 39422 pm11.6 39427 pm11.7 39431 opelopab4 39590 stoweidlem35 41040 mpt2mptx2 42974 |
Copyright terms: Public domain | W3C validator |