Theorem 2rexbii 3144

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

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

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 3093

This theorem is used by:  rexnal3  3151  3reeanv  3241  2nreu  4412  poxp2  8148  poxp3  8155  poseq  8163  1sdom  9225  ttrcltr  9695  addcompr  11024  mulcompr  11026  4fvwrd4  13695  ntrivcvgmul  15982  prodmo  16016  pythagtriplem2  16902  pythagtrip  16919  cat1  18179  isnsgrp  18810  efgrelexlemb  19851  ordthaus  23578  regr1lem2  23934  fmucndlem  24484  madeval2  28063  zaddscl  28624  zmulscld  28627  z12addscl  28707  dfcgra2  29178  axpasch  29328  axeuclid  29350  axcontlem4  29354  umgr2edg1  29598  wwlksnwwlksnon  30301  xrofsup  33149  constrcbvlem  34176  kardexen  35600  satfvsucsuc  35878  satf0  35885  altopelaltxp  36489  brsegle  36621  qdiffALT  38013  fimgmcyclem  43342  fimgmcyc  43343  mzpcompact2lem  43523  sbc4rex  43558  7rexfrabdioph  43568  expdiophlem1  43789  fourierdlem42  46904  prpair  48291  ldepslinc  49330  sepnsepolem1  49741