Theorem 2rexbii 3180

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

Syntax hints:   ↔ wb 196  ∃wrex 3051

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-rex 3056

This theorem is referenced by:  rexnal3  3182  ralnex2  3183  ralnex3  3184  3reeanv  3246  addcompr  10035  mulcompr  10037  4fvwrd4  12653  ntrivcvgmul  14833  prodmo  14865  pythagtriplem2  15724  pythagtrip  15741  isnsgrp  17489  efgrelexlemb  18363  ordthaus  21390  regr1lem2  21745  fmucndlem  22296  dfcgra2  25920  axpasch  26020  axeuclid  26042  axcontlem4  26046  umgr2edg1  26302  wwlksnwwlksnon  27033  xrofsup  29842  poseq  32059  madeval2  32242  altopelaltxp  32389  brsegle  32521  mzpcompact2lem  37816  sbc4rex  37855  7rexfrabdioph  37866  expdiophlem1  38090  fourierdlem42  40869  ldepslinc  42808