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 3070

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-rex 3071

This theorem is referenced by:  rexnal3  3129  3reeanv  3214  2nreu  4387  poseq  8037  1sdom  9105  ttrcltr  9565  addcompr  10870  mulcompr  10872  4fvwrd4  13469  ntrivcvgmul  15705  prodmo  15737  pythagtriplem2  16607  pythagtrip  16624  cat1  17901  isnsgrp  18468  efgrelexlemb  19443  ordthaus  22633  regr1lem2  22989  fmucndlem  23541  dfcgra2  27421  axpasch  27539  axeuclid  27561  axcontlem4  27565  umgr2edg1  27808  wwlksnwwlksnon  28509  xrofsup  31318  satfvsucsuc  33567  satf0  33574  poxp2  34016  poxp3  34022  madeval2  34128  altopelaltxp  34369  brsegle  34501  mzpcompact2lem  40823  sbc4rex  40861  7rexfrabdioph  40872  expdiophlem1  41094  fourierdlem42  44015  prpair  45293  ldepslinc  46190  sepnsepolem1  46555