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 1764 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1764 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: 3exbii 1766 3exdistr 1910 eeeanv 2171 ee4anv 2172 cbvex4v 2277 2sb5rf 2439 sbel2x 2447 2exsb 2457 2mo2 2538 rexcomf 3078 reean 3085 ceqsex3v 3219 ceqsex4v 3220 ceqsex8v 3222 vtocl3 3235 copsexg 4882 opelopabsbALT 4909 opabn0 4931 elxp2 5056 rabxp 5078 elxp3 5092 elvv 5100 elvvv 5101 copsex2gb 5153 elcnv2 5222 cnvuni 5231 xpdifid 5481 coass 5571 fununi 5878 dfmpt3 5927 tpres 6371 dfoprab2 6599 dmoprab 6639 rnoprab 6641 mpt2mptx 6649 resoprab 6654 elrnmpt2res 6672 ov3 6695 ov6g 6696 uniuni 6865 oprabex3 7048 wfrlem4 7305 oeeu 7570 xpassen 7939 zorn2lem6 9206 ltresr 9840 axaddf 9845 axmulf 9846 hashfun 13084 hash2prb 13111 5oalem7 27903 mpt2mptxf 28860 eulerpartlemgvv 29765 bnj600 30243 bnj916 30257 bnj983 30275 bnj986 30278 bnj996 30279 bnj1021 30288 elima4 30924 brtxp2 31158 brpprod3a 31163 brpprod3b 31164 elfuns 31192 brcart 31209 brimg 31214 brapply 31215 brsuccf 31218 brrestrict 31226 dfrdg4 31228 ellines 31429 bj-cbvex4vv 31930 itg2addnclem3 32633 dalem20 33997 dvhopellsm 35424 diblsmopel 35478 pm11.52 37608 2exanali 37609 pm11.6 37614 pm11.7 37618 opelopab4 37788 stoweidlem35 38928 mpt2mptx2 41906 |
Copyright terms: Public domain | W3C validator |