Theorem 2rexbii 3141

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

Syntax hints:   ↔ wb 209  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexnal3  3148  3reeanv  3238  2nreu  4410  poxp2  8140  poxp3  8147  poseq  8155  1sdom  9216  ttrcltr  9686  addcompr  11007  mulcompr  11009  4fvwrd4  13678  ntrivcvgmul  15958  prodmo  15992  pythagtriplem2  16878  pythagtrip  16895  cat1  18155  isnsgrp  18782  efgrelexlemb  19821  ordthaus  23522  regr1lem2  23878  fmucndlem  24428  madeval2  28007  zaddscl  28568  zmulscld  28571  z12addscl  28651  dfcgra2  29122  axpasch  29272  axeuclid  29294  axcontlem4  29298  umgr2edg1  29542  wwlksnwwlksnon  30245  xrofsup  33093  constrcbvlem  34126  kardexen  35557  satfvsucsuc  35838  satf0  35845  altopelaltxp  36449  brsegle  36581  qdiffALT  37953  fimgmcyclem  43284  fimgmcyc  43285  mzpcompact2lem  43465  sbc4rex  43500  7rexfrabdioph  43510  expdiophlem1  43731  fourierdlem42  46846  prpair  48233  ldepslinc  49272  sepnsepolem1  49683