Theorem 2rexbii 3130

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

Syntax hints:   ↔ wb 205  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexnal3  3137  3reeanv  3228  2nreu  4442  poxp2  8129  poxp3  8136  poseq  8144  1sdom  9248  ttrcltr  9711  addcompr  11016  mulcompr  11018  4fvwrd4  13621  ntrivcvgmul  15848  prodmo  15880  pythagtriplem2  16750  pythagtrip  16767  cat1  18047  isnsgrp  18614  efgrelexlemb  19618  ordthaus  22888  regr1lem2  23244  fmucndlem  23796  madeval2  27348  dfcgra2  28081  axpasch  28199  axeuclid  28221  axcontlem4  28225  umgr2edg1  28468  wwlksnwwlksnon  29169  xrofsup  31980  satfvsucsuc  34356  satf0  34363  altopelaltxp  34948  brsegle  35080  mzpcompact2lem  41489  sbc4rex  41527  7rexfrabdioph  41538  expdiophlem1  41760  fourierdlem42  44865  prpair  46169  ldepslinc  47190  sepnsepolem1  47554