Theorem 2rexbii 3119

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

Syntax hints:   ↔ wb 205  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061

This theorem is referenced by:  rexnal3  3126  3reeanv  3218  2nreu  4438  poxp2  8149  poxp3  8156  poseq  8164  1sdom  9275  ttrcltr  9752  addcompr  11055  mulcompr  11057  4fvwrd4  13669  ntrivcvgmul  15901  prodmo  15933  pythagtriplem2  16814  pythagtrip  16831  cat1  18114  isnsgrp  18711  efgrelexlemb  19744  ordthaus  23376  regr1lem2  23732  fmucndlem  24284  madeval2  27874  dfcgra2  28754  axpasch  28872  axeuclid  28894  axcontlem4  28898  umgr2edg1  29144  wwlksnwwlksnon  29846  xrofsup  32674  satfvsucsuc  35206  satf0  35213  altopelaltxp  35813  brsegle  35945  fimgmcyclem  42223  fimgmcyc  42224  mzpcompact2lem  42445  sbc4rex  42483  7rexfrabdioph  42494  expdiophlem1  42716  fourierdlem42  45806  prpair  47109  ldepslinc  47928  sepnsepolem1  48291