Theorem 2rexbii 3137

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

Syntax hints:   ↔ wb 208  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexnal3  3144  3reeanv  3234  2nreu  4397  poxp2  8118  poxp3  8125  poseq  8133  1sdom  9195  ttrcltr  9668  addcompr  10976  mulcompr  10978  4fvwrd4  13650  ntrivcvgmul  15915  prodmo  15949  pythagtriplem2  16836  pythagtrip  16853  cat1  18113  isnsgrp  18740  efgrelexlemb  19773  ordthaus  23424  regr1lem2  23780  fmucndlem  24330  madeval2  27903  zaddscl  28464  zmulscld  28467  z12addscl  28547  dfcgra2  28976  axpasch  29088  axeuclid  29110  axcontlem4  29114  umgr2edg1  29358  wwlksnwwlksnon  30061  xrofsup  32919  constrcbvlem  34013  satfvsucsuc  35679  satf0  35686  altopelaltxp  36290  brsegle  36422  qdiffALT  37784  fimgmcyclem  43115  fimgmcyc  43116  mzpcompact2lem  43296  sbc4rex  43331  7rexfrabdioph  43341  expdiophlem1  43562  fourierdlem42  46687  prpair  48071  ldepslinc  49095  sepnsepolem1  49507