Theorem 2rexbii 3129

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

Syntax hints:   ↔ wb 206  ∃wrex 3070

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 3071

This theorem is referenced by:  rexnal3  3136  3reeanv  3230  2nreu  4444  poxp2  8168  poxp3  8175  poseq  8183  1sdom  9284  ttrcltr  9756  addcompr  11061  mulcompr  11063  4fvwrd4  13688  ntrivcvgmul  15938  prodmo  15972  pythagtriplem2  16855  pythagtrip  16872  cat1  18142  isnsgrp  18736  efgrelexlemb  19768  ordthaus  23392  regr1lem2  23748  fmucndlem  24300  madeval2  27892  zaddscl  28380  zmulscld  28383  dfcgra2  28838  axpasch  28956  axeuclid  28978  axcontlem4  28982  umgr2edg1  29228  wwlksnwwlksnon  29935  xrofsup  32771  satfvsucsuc  35370  satf0  35377  altopelaltxp  35977  brsegle  36109  fimgmcyclem  42543  fimgmcyc  42544  mzpcompact2lem  42762  sbc4rex  42800  7rexfrabdioph  42811  expdiophlem1  43033  fourierdlem42  46164  prpair  47488  ldepslinc  48426  sepnsepolem1  48819