Theorem 2rexbii 3112

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

Syntax hints:   ↔ wb 206  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  rexnal3  3119  3reeanv  3209  2nreu  4396  poxp2  8085  poxp3  8092  poseq  8100  1sdom  9155  ttrcltr  9625  addcompr  10932  mulcompr  10934  4fvwrd4  13564  ntrivcvgmul  15825  prodmo  15859  pythagtriplem2  16745  pythagtrip  16762  cat1  18021  isnsgrp  18648  efgrelexlemb  19679  ordthaus  23328  regr1lem2  23684  fmucndlem  24234  madeval2  27829  zaddscl  28390  zmulscld  28393  z12addscl  28473  dfcgra2  28902  axpasch  29014  axeuclid  29036  axcontlem4  29040  umgr2edg1  29284  wwlksnwwlksnon  29988  xrofsup  32847  constrcbvlem  33912  satfvsucsuc  35559  satf0  35566  altopelaltxp  36170  brsegle  36302  fimgmcyclem  42784  fimgmcyc  42785  mzpcompact2lem  42989  sbc4rex  43027  7rexfrabdioph  43038  expdiophlem1  43259  fourierdlem42  46389  prpair  47743  ldepslinc  48751  sepnsepolem1  49163