Theorem 2rexbii 3189

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

Syntax hints:   ↔ wb 198  ∃wrex 3083

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3088

This theorem is referenced by:  rexnal3  3199  ralnex2OLD  3201  ralnex3OLD  3203  3reeanv  3303  2nreu  4270  addcompr  10233  mulcompr  10235  4fvwrd4  12836  ntrivcvgmul  15108  prodmo  15140  pythagtriplem2  16000  pythagtrip  16017  isnsgrp  17746  efgrelexlemb  18626  ordthaus  21686  regr1lem2  22042  fmucndlem  22593  dfcgra2  26308  axpasch  26420  axeuclid  26442  axcontlem4  26446  umgr2edg1  26686  wwlksnwwlksnon  27411  xrofsup  30233  poseq  32556  madeval2  32751  altopelaltxp  32898  brsegle  33030  mzpcompact2lem  38688  sbc4rex  38727  7rexfrabdioph  38738  expdiophlem1  38959  fourierdlem42  41811  prpair  42971  ldepslinc  43871