Theorem 2rexbii 3182

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

Syntax hints:   ↔ wb 205  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  rexnal3  3188  3reeanv  3295  2nreu  4375  ttrcltr  9474  addcompr  10777  mulcompr  10779  4fvwrd4  13376  ntrivcvgmul  15614  prodmo  15646  pythagtriplem2  16518  pythagtrip  16535  cat1  17812  isnsgrp  18379  efgrelexlemb  19356  ordthaus  22535  regr1lem2  22891  fmucndlem  23443  dfcgra2  27191  axpasch  27309  axeuclid  27331  axcontlem4  27335  umgr2edg1  27578  wwlksnwwlksnon  28280  xrofsup  31090  satfvsucsuc  33327  satf0  33334  poxp2  33790  poxp3  33796  poseq  33802  madeval2  34037  altopelaltxp  34278  brsegle  34410  mzpcompact2lem  40573  sbc4rex  40611  7rexfrabdioph  40622  expdiophlem1  40843  fourierdlem42  43690  prpair  44953  ldepslinc  45850  sepnsepolem1  46215