Theorem 2rexbii 3141

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 3112	. 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
3	2	rexbii 3112	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 209  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexnal3  3148  3reeanv  3238  2nreu  4401  poxp2  8127  poxp3  8134  poseq  8142  1sdom  9203  ttrcltr  9673  addcompr  10994  mulcompr  10996  4fvwrd4  13667  ntrivcvgmul  15946  prodmo  15980  pythagtriplem2  16867  pythagtrip  16884  cat1  18144  isnsgrp  18771  efgrelexlemb  19811  ordthaus  23502  regr1lem2  23858  fmucndlem  24408  madeval2  27984  zaddscl  28545  zmulscld  28548  z12addscl  28628  dfcgra2  29082  axpasch  29200  axeuclid  29222  axcontlem4  29226  umgr2edg1  29470  wwlksnwwlksnon  30173  xrofsup  33024  constrcbvlem  34062  satfvsucsuc  35728  satf0  35735  altopelaltxp  36339  brsegle  36471  qdiffALT  37832  fimgmcyclem  43163  fimgmcyc  43164  mzpcompact2lem  43344  sbc4rex  43379  7rexfrabdioph  43389  expdiophlem1  43610  fourierdlem42  46721  prpair  48105  ldepslinc  49140  sepnsepolem1  49551