Theorem 2rexbii 3108

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

Syntax hints:   ↔ wb 206  ∃wrex 3056

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 3057

This theorem is referenced by:  rexnal3  3115  3reeanv  3205  2nreu  4394  poxp2  8073  poxp3  8080  poseq  8088  1sdom  9139  ttrcltr  9606  addcompr  10909  mulcompr  10911  4fvwrd4  13545  ntrivcvgmul  15806  prodmo  15840  pythagtriplem2  16726  pythagtrip  16743  cat1  18001  isnsgrp  18628  efgrelexlemb  19660  ordthaus  23297  regr1lem2  23653  fmucndlem  24203  madeval2  27792  zaddscl  28316  zmulscld  28319  zs12addscl  28385  dfcgra2  28806  axpasch  28917  axeuclid  28939  axcontlem4  28943  umgr2edg1  29187  wwlksnwwlksnon  29891  xrofsup  32745  constrcbvlem  33763  satfvsucsuc  35397  satf0  35404  altopelaltxp  36009  brsegle  36141  fimgmcyclem  42565  fimgmcyc  42566  mzpcompact2lem  42783  sbc4rex  42821  7rexfrabdioph  42832  expdiophlem1  43053  fourierdlem42  46186  prpair  47531  ldepslinc  48540  sepnsepolem1  48952