Theorem 2rexbii 3127

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

Syntax hints:   ↔ wb 206  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  rexnal3  3134  3reeanv  3228  2nreu  4450  poxp2  8167  poxp3  8174  poseq  8182  1sdom  9282  ttrcltr  9754  addcompr  11059  mulcompr  11061  4fvwrd4  13685  ntrivcvgmul  15935  prodmo  15969  pythagtriplem2  16851  pythagtrip  16868  cat1  18151  isnsgrp  18749  efgrelexlemb  19783  ordthaus  23408  regr1lem2  23764  fmucndlem  24316  madeval2  27907  zaddscl  28395  zmulscld  28398  dfcgra2  28853  axpasch  28971  axeuclid  28993  axcontlem4  28997  umgr2edg1  29243  wwlksnwwlksnon  29945  xrofsup  32778  satfvsucsuc  35350  satf0  35357  altopelaltxp  35958  brsegle  36090  fimgmcyclem  42520  fimgmcyc  42521  mzpcompact2lem  42739  sbc4rex  42777  7rexfrabdioph  42788  expdiophlem1  43010  fourierdlem42  46105  prpair  47426  ldepslinc  48355  sepnsepolem1  48718