Theorem 2rexbii 3142

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

Hypothesis

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

Assertion

Ref	Expression
2rexbii	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2rexbii

Step	Hyp	Ref	Expression
1		2rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	rexbii 3113	. 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
3	2	rexbii 3113	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   ↔ wb 209  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  rexnal3  3149  3reeanv  3239  2nreu  4405  poxp2  8190  poxp3  8197  poseq  8205  1sdom  9277  ttrcltr  9747  addcompr  11136  mulcompr  11138  4fvwrd4  13812  ntrivcvgmul  16103  prodmo  16135  pythagtriplem2  17027  pythagtrip  17044  cat1  18304  isnsgrp  18944  efgrelexlemb  19997  ordthaus  23735  regr1lem2  24092  fmucndlem  24642  madeval2  28252  zaddscl  28813  zmulscld  28816  z12addscl  28896  dfcgra2  29371  axpasch  29552  axeuclid  29574  axcontlem4  29578  umgr2edg1  29825  wwlksnwwlksnon  30537  xrofsup  33432  constrcbvlem  34470  kardexen  35944  satfvsucsuc  36310  satf0  36317  altopelaltxp  36932  brsegle  37064  qdiffALT  38454  fimgmcyclem  43801  fimgmcyc  43802  mzpcompact2lem  43966  sbc4rex  44001  7rexfrabdioph  44011  expdiophlem1  44232  fourierdlem42  47374  prpair  48798  ldepslinc  49836  sepnsepolem1  50251