Theorem 2rexbii 3116

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

Syntax hints:   ↔ wb 207  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexnal3  3123  3reeanv  3213  2nreu  4379  poxp2  8090  poxp3  8097  poseq  8105  1sdom  9162  ttrcltr  9635  addcompr  10942  mulcompr  10944  4fvwrd4  13600  ntrivcvgmul  15865  prodmo  15899  pythagtriplem2  16786  pythagtrip  16803  cat1  18062  isnsgrp  18689  efgrelexlemb  19723  ordthaus  23374  regr1lem2  23730  fmucndlem  24280  madeval2  27850  zaddscl  28411  zmulscld  28414  z12addscl  28494  dfcgra2  28923  axpasch  29035  axeuclid  29057  axcontlem4  29061  umgr2edg1  29305  wwlksnwwlksnon  30008  xrofsup  32866  constrcbvlem  33946  satfvsucsuc  35600  satf0  35607  altopelaltxp  36211  brsegle  36343  qdiffALT  37695  fimgmcyclem  43026  fimgmcyc  43027  mzpcompact2lem  43207  sbc4rex  43242  7rexfrabdioph  43252  expdiophlem1  43473  fourierdlem42  46599  prpair  47983  ldepslinc  49007  sepnsepolem1  49419