Theorem 2rexbii 3138

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

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexnal3  3145  3reeanv  3235  2nreu  4401  poxp2  8162  poxp3  8169  poseq  8177  1sdom  9249  ttrcltr  9720  addcompr  11109  mulcompr  11111  4fvwrd4  13785  ntrivcvgmul  16076  prodmo  16108  pythagtriplem2  17000  pythagtrip  17017  cat1  18277  isnsgrp  18917  efgrelexlemb  19969  ordthaus  23707  regr1lem2  24064  fmucndlem  24614  madeval2  28224  zaddscl  28785  zmulscld  28788  z12addscl  28868  dfcgra2  29343  axpasch  29524  axeuclid  29546  axcontlem4  29550  umgr2edg1  29797  wwlksnwwlksnon  30509  xrofsup  33405  constrcbvlem  34433  kardexen  35887  satfvsucsuc  36216  satf0  36223  altopelaltxp  36833  brsegle  36965  qdiffALT  38342  fimgmcyclem  43690  fimgmcyc  43691  mzpcompact2lem  43855  sbc4rex  43890  7rexfrabdioph  43900  expdiophlem1  44121  fourierdlem42  47252  prpair  48676  ldepslinc  49714  sepnsepolem1  50129