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

Syntax hints:   ↔ wb 206  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  rexnal3  3123  3reeanv  3214  2nreu  4419  poxp2  8142  poxp3  8149  poseq  8157  1sdom  9256  ttrcltr  9730  addcompr  11035  mulcompr  11037  4fvwrd4  13665  ntrivcvgmul  15918  prodmo  15952  pythagtriplem2  16837  pythagtrip  16854  cat1  18110  isnsgrp  18701  efgrelexlemb  19731  ordthaus  23322  regr1lem2  23678  fmucndlem  24229  madeval2  27813  zaddscl  28334  zmulscld  28337  dfcgra2  28809  axpasch  28920  axeuclid  28942  axcontlem4  28946  umgr2edg1  29190  wwlksnwwlksnon  29897  xrofsup  32744  constrcbvlem  33789  satfvsucsuc  35387  satf0  35394  altopelaltxp  35994  brsegle  36126  fimgmcyclem  42556  fimgmcyc  42557  mzpcompact2lem  42774  sbc4rex  42812  7rexfrabdioph  42823  expdiophlem1  43045  fourierdlem42  46178  prpair  47515  ldepslinc  48485  sepnsepolem1  48896