Theorem 2exbii 1815

Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Hypothesis

Ref	Expression
2exbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2exbii	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		2exbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1814	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1814	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 196  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777

This theorem depends on definitions:  df-bi 197  df-ex 1745

This theorem is referenced by:  3exbii  1816  3exdistr  1926  eeeanv  2219  ee4anv  2220  cbvex4v  2325  2sb5rf  2479  sbel2x  2487  2exsb  2497  2mo2  2579  rexcomf  3126  reean  3135  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  vtocl3  3293  copsexg  4985  opelopabsbALT  5013  opabn0  5035  elxp2  5166  rabxp  5188  elxp3  5203  elvv  5211  elvvv  5212  copsex2gb  5263  elcnv2  5332  cnvuni  5341  xpdifid  5597  coass  5692  fununi  6002  dfmpt3  6052  tpres  6507  dfoprab2  6743  dmoprab  6783  rnoprab  6785  mpt2mptx  6793  resoprab  6798  elrnmpt2res  6816  ov3  6839  ov6g  6840  uniuni  7013  oprabex3  7199  wfrlem4  7463  oeeu  7728  xpassen  8095  zorn2lem6  9361  ltresr  9999  axaddf  10004  axmulf  10005  hashfun  13262  hash2prb  13292  5oalem7  28647  mpt2mptxf  29605  eulerpartlemgvv  30566  bnj600  31115  bnj916  31129  bnj983  31147  bnj986  31150  bnj996  31151  bnj1021  31160  elima4  31803  brtxp2  32113  brpprod3a  32118  brpprod3b  32119  elfuns  32147  brcart  32164  brimg  32169  brapply  32170  brsuccf  32173  brrestrict  32181  dfrdg4  32183  ellines  32384  bj-cbvex4vv  32868  itg2addnclem3  33593  brxrn2  34277  dfxrn2  34278  ecxrn  34289  inxpxrn  34293  rnxrn  34296  dalem20  35297  dvhopellsm  36723  diblsmopel  36777  pm11.52  38903  2exanali  38904  pm11.6  38909  pm11.7  38913  opelopab4  39084  stoweidlem35  40570  mpt2mptx2  42438