Theorem 2rexbii 3105

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

Syntax hints:   ↔ wb 206  ∃wrex 3053

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 3054

This theorem is referenced by:  rexnal3  3112  3reeanv  3202  2nreu  4397  poxp2  8083  poxp3  8090  poseq  8098  1sdom  9154  ttrcltr  9631  addcompr  10934  mulcompr  10936  4fvwrd4  13569  ntrivcvgmul  15827  prodmo  15861  pythagtriplem2  16747  pythagtrip  16764  cat1  18022  isnsgrp  18615  efgrelexlemb  19647  ordthaus  23287  regr1lem2  23643  fmucndlem  24194  madeval2  27781  zaddscl  28305  zmulscld  28308  zs12addscl  28372  dfcgra2  28793  axpasch  28904  axeuclid  28926  axcontlem4  28930  umgr2edg1  29174  wwlksnwwlksnon  29878  xrofsup  32723  constrcbvlem  33721  satfvsucsuc  35337  satf0  35344  altopelaltxp  35949  brsegle  36081  fimgmcyclem  42506  fimgmcyc  42507  mzpcompact2lem  42724  sbc4rex  42762  7rexfrabdioph  42773  expdiophlem1  42994  fourierdlem42  46131  prpair  47486  ldepslinc  48495  sepnsepolem1  48907