Theorem 2rexbii 3211

Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)

Hypothesis

Ref	Expression
rexbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2rexbii	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2rexbii

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	rexbii 3210	. 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
3	2	rexbii 3210	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 209  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  rexnal3  3220  3reeanv  3321  2nreu  4349  addcompr  10432  mulcompr  10434  4fvwrd4  13022  ntrivcvgmul  15250  prodmo  15282  pythagtriplem2  16144  pythagtrip  16161  isnsgrp  17897  efgrelexlemb  18868  ordthaus  21989  regr1lem2  22345  fmucndlem  22897  dfcgra2  26624  axpasch  26735  axeuclid  26757  axcontlem4  26761  umgr2edg1  27001  wwlksnwwlksnon  27701  xrofsup  30518  satfvsucsuc  32725  satf0  32732  poseq  33208  madeval2  33403  altopelaltxp  33550  brsegle  33682  mzpcompact2lem  39692  sbc4rex  39730  7rexfrabdioph  39741  expdiophlem1  39962  fourierdlem42  42791  prpair  44018  ldepslinc  44918