Theorem 2rexbii 3129

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

Syntax hints:   ↔ wb 205  ∃wrex 3070

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 3071

This theorem is referenced by:  rexnal3  3136  3reeanv  3227  2nreu  4441  poxp2  8131  poxp3  8138  poseq  8146  1sdom  9250  ttrcltr  9713  addcompr  11018  mulcompr  11020  4fvwrd4  13623  ntrivcvgmul  15850  prodmo  15882  pythagtriplem2  16752  pythagtrip  16769  cat1  18049  isnsgrp  18616  efgrelexlemb  19620  ordthaus  22895  regr1lem2  23251  fmucndlem  23803  madeval2  27356  dfcgra2  28119  axpasch  28237  axeuclid  28259  axcontlem4  28263  umgr2edg1  28506  wwlksnwwlksnon  29207  xrofsup  32018  satfvsucsuc  34425  satf0  34432  altopelaltxp  35017  brsegle  35149  mzpcompact2lem  41571  sbc4rex  41609  7rexfrabdioph  41620  expdiophlem1  41842  fourierdlem42  44944  prpair  46248  ldepslinc  47268  sepnsepolem1  47632