Theorem 2rexbii 3139

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  rexnal3  3146  3reeanv  3236  2nreu  4402  poxp2  8144  poxp3  8151  poseq  8159  1sdom  9230  ttrcltr  9701  addcompr  11087  mulcompr  11089  4fvwrd4  13762  ntrivcvgmul  16051  prodmo  16083  pythagtriplem2  16975  pythagtrip  16992  cat1  18252  isnsgrp  18892  efgrelexlemb  19944  ordthaus  23682  regr1lem2  24039  fmucndlem  24589  madeval2  28201  zaddscl  28762  zmulscld  28765  z12addscl  28845  dfcgra2  29320  axpasch  29501  axeuclid  29523  axcontlem4  29527  umgr2edg1  29774  wwlksnwwlksnon  30486  xrofsup  33341  constrcbvlem  34369  kardexen  35804  satfvsucsuc  36099  satf0  36106  altopelaltxp  36711  brsegle  36843  qdiffALT  38217  fimgmcyclem  43559  fimgmcyc  43560  mzpcompact2lem  43715  sbc4rex  43750  7rexfrabdioph  43760  expdiophlem1  43981  fourierdlem42  47103  prpair  48527  ldepslinc  49565  sepnsepolem1  49974