Theorem 2rexbii 3140

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  rexnal3  3147  3reeanv  3237  2nreu  4405  poxp2  8145  poxp3  8152  poseq  8160  1sdom  9229  ttrcltr  9699  addcompr  11034  mulcompr  11036  4fvwrd4  13707  ntrivcvgmul  15995  prodmo  16029  pythagtriplem2  16915  pythagtrip  16932  cat1  18192  isnsgrp  18831  efgrelexlemb  19883  ordthaus  23615  regr1lem2  23972  fmucndlem  24522  madeval2  28106  zaddscl  28667  zmulscld  28670  z12addscl  28750  dfcgra2  29225  axpasch  29406  axeuclid  29428  axcontlem4  29432  umgr2edg1  29679  wwlksnwwlksnon  30391  xrofsup  33246  constrcbvlem  34273  kardexen  35697  satfvsucsuc  35952  satf0  35959  altopelaltxp  36564  brsegle  36696  qdiffALT  38088  fimgmcyclem  43423  fimgmcyc  43424  mzpcompact2lem  43604  sbc4rex  43639  7rexfrabdioph  43649  expdiophlem1  43870  fourierdlem42  46985  prpair  48409  ldepslinc  49447  sepnsepolem1  49856