Theorem 2rexbii 3251

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

Syntax hints:   ↔ wb 208  ∃wrex 3142

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 209  df-an 399  df-ex 1780  df-rex 3147

This theorem is referenced by:  rexnal3  3262  ralnex2OLD  3264  ralnex3OLD  3266  3reeanv  3371  2nreu  4396  addcompr  10446  mulcompr  10448  4fvwrd4  13030  ntrivcvgmul  15261  prodmo  15293  pythagtriplem2  16157  pythagtrip  16174  isnsgrp  17908  efgrelexlemb  18879  ordthaus  21995  regr1lem2  22351  fmucndlem  22903  dfcgra2  26619  axpasch  26730  axeuclid  26752  axcontlem4  26756  umgr2edg1  26996  wwlksnwwlksnon  27697  xrofsup  30495  satfvsucsuc  32616  satf0  32623  poseq  33099  madeval2  33294  altopelaltxp  33441  brsegle  33573  mzpcompact2lem  39354  sbc4rex  39392  7rexfrabdioph  39403  expdiophlem1  39624  fourierdlem42  42441  prpair  43670  ldepslinc  44571