Theorem 2rexbii 3114

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

Syntax hints:   ↔ wb 206  ∃wrex 3062

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 3063

This theorem is referenced by:  rexnal3  3121  3reeanv  3211  2nreu  4385  poxp2  8086  poxp3  8093  poseq  8101  1sdom  9158  ttrcltr  9628  addcompr  10935  mulcompr  10937  4fvwrd4  13593  ntrivcvgmul  15858  prodmo  15892  pythagtriplem2  16779  pythagtrip  16796  cat1  18055  isnsgrp  18682  efgrelexlemb  19716  ordthaus  23359  regr1lem2  23715  fmucndlem  24265  madeval2  27839  zaddscl  28400  zmulscld  28403  z12addscl  28483  dfcgra2  28912  axpasch  29024  axeuclid  29046  axcontlem4  29050  umgr2edg1  29294  wwlksnwwlksnon  29998  xrofsup  32855  constrcbvlem  33915  satfvsucsuc  35563  satf0  35570  altopelaltxp  36174  brsegle  36306  fimgmcyclem  42992  fimgmcyc  42993  mzpcompact2lem  43197  sbc4rex  43235  7rexfrabdioph  43246  expdiophlem1  43467  fourierdlem42  46595  prpair  47973  ldepslinc  48997  sepnsepolem1  49409