Theorem 2rexbii 3109

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

Syntax hints:   ↔ wb 206  ∃wrex 3057

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 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexnal3  3116  3reeanv  3206  2nreu  4393  poxp2  8079  poxp3  8086  poseq  8094  1sdom  9146  ttrcltr  9613  addcompr  10919  mulcompr  10921  4fvwrd4  13550  ntrivcvgmul  15811  prodmo  15845  pythagtriplem2  16731  pythagtrip  16748  cat1  18006  isnsgrp  18633  efgrelexlemb  19664  ordthaus  23300  regr1lem2  23656  fmucndlem  24206  madeval2  27795  zaddscl  28319  zmulscld  28322  zs12addscl  28388  dfcgra2  28809  axpasch  28921  axeuclid  28943  axcontlem4  28947  umgr2edg1  29191  wwlksnwwlksnon  29895  xrofsup  32754  constrcbvlem  33789  satfvsucsuc  35430  satf0  35437  altopelaltxp  36041  brsegle  36173  fimgmcyclem  42652  fimgmcyc  42653  mzpcompact2lem  42869  sbc4rex  42907  7rexfrabdioph  42918  expdiophlem1  43139  fourierdlem42  46272  prpair  47626  ldepslinc  48635  sepnsepolem1  49047