Theorem 2exbii 1775

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 1774	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1774	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 196  ∃wex 1704

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

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

This theorem is referenced by:  3exbii  1776  3exdistr  1923  eeeanv  2183  ee4anv  2184  cbvex4v  2289  2sb5rf  2451  sbel2x  2459  2exsb  2469  2mo2  2550  rexcomf  3097  reean  3106  ceqsex3v  3246  ceqsex4v  3247  ceqsex8v  3249  vtocl3  3262  copsexg  4956  opelopabsbALT  4984  opabn0  5006  elxp2  5132  rabxp  5154  elxp3  5169  elvv  5177  elvvv  5178  copsex2gb  5230  elcnv2  5300  cnvuni  5309  xpdifid  5562  coass  5654  fununi  5964  dfmpt3  6014  tpres  6466  dfoprab2  6701  dmoprab  6741  rnoprab  6743  mpt2mptx  6751  resoprab  6756  elrnmpt2res  6774  ov3  6797  ov6g  6798  uniuni  6971  oprabex3  7157  wfrlem4  7418  oeeu  7683  xpassen  8054  zorn2lem6  9323  ltresr  9961  axaddf  9966  axmulf  9967  hashfun  13224  hash2prb  13254  5oalem7  28519  mpt2mptxf  29477  eulerpartlemgvv  30438  bnj600  30989  bnj916  31003  bnj983  31021  bnj986  31024  bnj996  31025  bnj1021  31034  elima4  31679  brtxp2  31988  brpprod3a  31993  brpprod3b  31994  elfuns  32022  brcart  32039  brimg  32044  brapply  32045  brsuccf  32048  brrestrict  32056  dfrdg4  32058  ellines  32259  bj-cbvex4vv  32743  itg2addnclem3  33463  dalem20  34979  dvhopellsm  36406  diblsmopel  36460  pm11.52  38586  2exanali  38587  pm11.6  38592  pm11.7  38596  opelopab4  38767  stoweidlem35  40252  mpt2mptx2  42113