Theorem 2rexbii 3230

Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)

Hypothesis

Ref	Expression
rexbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2rexbii	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2rexbii

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	rexbii 3229	. 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
3	2	rexbii 3229	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 197  ∃wrex 3097

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

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-rex 3102

This theorem is referenced by:  rexnal3  3232  ralnex2  3233  ralnex3  3234  3reeanv  3296  addcompr  10128  mulcompr  10130  4fvwrd4  12683  ntrivcvgmul  14855  prodmo  14887  pythagtriplem2  15739  pythagtrip  15756  isnsgrp  17493  efgrelexlemb  18364  ordthaus  21402  regr1lem2  21757  fmucndlem  22308  dfcgra2  25935  axpasch  26035  axeuclid  26057  axcontlem4  26061  umgr2edg1  26318  wwlksnwwlksnon  27053  xrofsup  29860  poseq  32074  madeval2  32257  altopelaltxp  32404  brsegle  32536  mzpcompact2lem  37816  sbc4rex  37855  7rexfrabdioph  37866  expdiophlem1  38089  fourierdlem42  40845  ldepslinc  42866