Theorem 2rexbii 3128

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

Syntax hints:   ↔ wb 208  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-rex 3077

This theorem is referenced by:  rexnal3  3135  3reeanv  3225  2nreu  4388  poxp2  8107  poxp3  8114  poseq  8122  1sdom  9184  ttrcltr  9657  addcompr  10965  mulcompr  10967  4fvwrd4  13639  ntrivcvgmul  15904  prodmo  15938  pythagtriplem2  16825  pythagtrip  16842  cat1  18102  isnsgrp  18729  efgrelexlemb  19762  ordthaus  23413  regr1lem2  23769  fmucndlem  24319  madeval2  27892  zaddscl  28453  zmulscld  28456  z12addscl  28536  dfcgra2  28965  axpasch  29077  axeuclid  29099  axcontlem4  29103  umgr2edg1  29347  wwlksnwwlksnon  30050  xrofsup  32908  constrcbvlem  33996  satfvsucsuc  35653  satf0  35660  altopelaltxp  36264  brsegle  36396  qdiffALT  37758  fimgmcyclem  43089  fimgmcyc  43090  mzpcompact2lem  43270  sbc4rex  43305  7rexfrabdioph  43315  expdiophlem1  43536  fourierdlem42  46661  prpair  48045  ldepslinc  49069  sepnsepolem1  49481