Theorem 2rexbii 3042

Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)

Hypothesis

Ref	Expression
rexbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2rexbii	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2rexbii

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	rexbii 3041	. 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
3	2	rexbii 3041	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 196  ∃wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  rexnal3  3044  ralnex2  3045  ralnex3  3046  3reeanv  3108  addcompr  9843  mulcompr  9845  4fvwrd4  12459  ntrivcvgmul  14634  prodmo  14666  pythagtriplem2  15522  pythagtrip  15539  isnsgrp  17288  efgrelexlemb  18163  ordthaus  21188  regr1lem2  21543  fmucndlem  22095  dfcgra2  25721  axpasch  25821  axeuclid  25843  axcontlem4  25847  umgr2edg1  26103  xrofsup  29533  poseq  31750  madeval2  31936  altopelaltxp  32083  brsegle  32215  mzpcompact2lem  37314  sbc4rex  37353  7rexfrabdioph  37364  expdiophlem1  37588  fourierdlem42  40366  ldepslinc  42298