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  4398  poxp2  8095  poxp3  8102  poseq  8110  1sdom  9167  ttrcltr  9637  addcompr  10944  mulcompr  10946  4fvwrd4  13576  ntrivcvgmul  15837  prodmo  15871  pythagtriplem2  16757  pythagtrip  16774  cat1  18033  isnsgrp  18660  efgrelexlemb  19691  ordthaus  23340  regr1lem2  23696  fmucndlem  24246  madeval2  27841  zaddscl  28402  zmulscld  28405  z12addscl  28485  dfcgra2  28914  axpasch  29026  axeuclid  29048  axcontlem4  29052  umgr2edg1  29296  wwlksnwwlksnon  30000  xrofsup  32857  constrcbvlem  33932  satfvsucsuc  35578  satf0  35585  altopelaltxp  36189  brsegle  36321  fimgmcyclem  42897  fimgmcyc  42898  mzpcompact2lem  43102  sbc4rex  43140  7rexfrabdioph  43151  expdiophlem1  43372  fourierdlem42  46501  prpair  47855  ldepslinc  48863  sepnsepolem1  49275