Theorem 2rexbii 3178

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

Syntax hints:   ↔ wb 205  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  rexnal3  3187  3reeanv  3293  2nreu  4372  addcompr  10708  mulcompr  10710  4fvwrd4  13305  ntrivcvgmul  15542  prodmo  15574  pythagtriplem2  16446  pythagtrip  16463  cat1  17728  isnsgrp  18294  efgrelexlemb  19271  ordthaus  22443  regr1lem2  22799  fmucndlem  23351  dfcgra2  27095  axpasch  27212  axeuclid  27234  axcontlem4  27238  umgr2edg1  27481  wwlksnwwlksnon  28181  xrofsup  30992  satfvsucsuc  33227  satf0  33234  ttrcltr  33702  poxp2  33717  poxp3  33723  poseq  33729  madeval2  33964  altopelaltxp  34205  brsegle  34337  mzpcompact2lem  40489  sbc4rex  40527  7rexfrabdioph  40538  expdiophlem1  40759  fourierdlem42  43580  prpair  44841  ldepslinc  45738  sepnsepolem1  46103