Theorem 2rexbii 3124

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

Syntax hints:   ↔ wb 205  ∃wrex 3069

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 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  rexnal3  3129  3reeanv  3216  2nreu  4406  poxp2  8080  poxp3  8087  poseq  8095  1sdom  9199  ttrcltr  9661  addcompr  10966  mulcompr  10968  4fvwrd4  13571  ntrivcvgmul  15798  prodmo  15830  pythagtriplem2  16700  pythagtrip  16717  cat1  17997  isnsgrp  18564  efgrelexlemb  19546  ordthaus  22772  regr1lem2  23128  fmucndlem  23680  madeval2  27226  dfcgra2  27835  axpasch  27953  axeuclid  27975  axcontlem4  27979  umgr2edg1  28222  wwlksnwwlksnon  28923  xrofsup  31740  satfvsucsuc  34046  satf0  34053  altopelaltxp  34637  brsegle  34769  mzpcompact2lem  41132  sbc4rex  41170  7rexfrabdioph  41181  expdiophlem1  41403  fourierdlem42  44510  prpair  45813  ldepslinc  46710  sepnsepolem1  47074