Theorem 2rexbii 3250

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

Syntax hints:   ↔ wb 208  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-rex 3146

This theorem is referenced by:  rexnal3  3261  ralnex2OLD  3263  ralnex3OLD  3265  3reeanv  3370  2nreu  4395  addcompr  10445  mulcompr  10447  4fvwrd4  13030  ntrivcvgmul  15260  prodmo  15292  pythagtriplem2  16156  pythagtrip  16173  isnsgrp  17907  efgrelexlemb  18878  ordthaus  21994  regr1lem2  22350  fmucndlem  22902  dfcgra2  26618  axpasch  26729  axeuclid  26751  axcontlem4  26755  umgr2edg1  26995  wwlksnwwlksnon  27696  xrofsup  30494  satfvsucsuc  32614  satf0  32621  poseq  33097  madeval2  33292  altopelaltxp  33439  brsegle  33571  mzpcompact2lem  39355  sbc4rex  39393  7rexfrabdioph  39404  expdiophlem1  39625  fourierdlem42  42441  prpair  43670  ldepslinc  44571