Theorem 2rexbii 3110

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

Syntax hints:   ↔ wb 206  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  rexnal3  3117  3reeanv  3211  2nreu  4410  poxp2  8125  poxp3  8132  poseq  8140  1sdom  9202  ttrcltr  9676  addcompr  10981  mulcompr  10983  4fvwrd4  13616  ntrivcvgmul  15875  prodmo  15909  pythagtriplem2  16795  pythagtrip  16812  cat1  18066  isnsgrp  18657  efgrelexlemb  19687  ordthaus  23278  regr1lem2  23634  fmucndlem  24185  madeval2  27768  zaddscl  28289  zmulscld  28292  dfcgra2  28764  axpasch  28875  axeuclid  28897  axcontlem4  28901  umgr2edg1  29145  wwlksnwwlksnon  29852  xrofsup  32697  constrcbvlem  33752  satfvsucsuc  35359  satf0  35366  altopelaltxp  35971  brsegle  36103  fimgmcyclem  42528  fimgmcyc  42529  mzpcompact2lem  42746  sbc4rex  42784  7rexfrabdioph  42795  expdiophlem1  43017  fourierdlem42  46154  prpair  47506  ldepslinc  48502  sepnsepolem1  48914