Theorem 2rexbii 3114

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

Syntax hints:   ↔ wb 206  ∃wrex 3059

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  rexnal3  3121  3reeanv  3212  2nreu  4417  poxp2  8137  poxp3  8144  poseq  8152  1sdom  9251  ttrcltr  9723  addcompr  11028  mulcompr  11030  4fvwrd4  13655  ntrivcvgmul  15907  prodmo  15941  pythagtriplem2  16824  pythagtrip  16841  cat1  18097  isnsgrp  18688  efgrelexlemb  19718  ordthaus  23309  regr1lem2  23665  fmucndlem  24216  madeval2  27797  zaddscl  28285  zmulscld  28288  dfcgra2  28743  axpasch  28854  axeuclid  28876  axcontlem4  28880  umgr2edg1  29124  wwlksnwwlksnon  29831  xrofsup  32681  constrcbvlem  33724  satfvsucsuc  35316  satf0  35323  altopelaltxp  35923  brsegle  36055  fimgmcyclem  42488  fimgmcyc  42489  mzpcompact2lem  42706  sbc4rex  42744  7rexfrabdioph  42755  expdiophlem1  42977  fourierdlem42  46114  prpair  47441  ldepslinc  48379  sepnsepolem1  48790