Theorem 2rexbii 3113

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 206  ∃wrex 3061

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 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexnal3  3120  3reeanv  3210  2nreu  4384  poxp2  8093  poxp3  8100  poseq  8108  1sdom  9165  ttrcltr  9637  addcompr  10944  mulcompr  10946  4fvwrd4  13602  ntrivcvgmul  15867  prodmo  15901  pythagtriplem2  16788  pythagtrip  16805  cat1  18064  isnsgrp  18691  efgrelexlemb  19725  ordthaus  23349  regr1lem2  23705  fmucndlem  24255  madeval2  27825  zaddscl  28386  zmulscld  28389  z12addscl  28469  dfcgra2  28898  axpasch  29010  axeuclid  29032  axcontlem4  29036  umgr2edg1  29280  wwlksnwwlksnon  29983  xrofsup  32840  constrcbvlem  33899  satfvsucsuc  35547  satf0  35554  altopelaltxp  36158  brsegle  36290  qdiffALT  37642  fimgmcyclem  42978  fimgmcyc  42979  mzpcompact2lem  43183  sbc4rex  43218  7rexfrabdioph  43228  expdiophlem1  43449  fourierdlem42  46577  prpair  47961  ldepslinc  48985  sepnsepolem1  49397