Theorem 2rexbii 3135

Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)

Hypothesis

Ref	Expression
2rexbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2rexbii	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2rexbii

Step	Hyp	Ref	Expression
1		2rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	rexbii 3100	. 2 ⊢ (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
3	2	rexbii 3100	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 206  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexnal3  3142  3reeanv  3236  2nreu  4467  poxp2  8184  poxp3  8191  poseq  8199  1sdom  9311  ttrcltr  9785  addcompr  11090  mulcompr  11092  4fvwrd4  13705  ntrivcvgmul  15950  prodmo  15984  pythagtriplem2  16864  pythagtrip  16881  cat1  18164  isnsgrp  18761  efgrelexlemb  19792  ordthaus  23413  regr1lem2  23769  fmucndlem  24321  madeval2  27910  zaddscl  28398  zmulscld  28401  dfcgra2  28856  axpasch  28974  axeuclid  28996  axcontlem4  29000  umgr2edg1  29246  wwlksnwwlksnon  29948  xrofsup  32774  satfvsucsuc  35333  satf0  35340  altopelaltxp  35940  brsegle  36072  fimgmcyclem  42488  fimgmcyc  42489  mzpcompact2lem  42707  sbc4rex  42745  7rexfrabdioph  42756  expdiophlem1  42978  fourierdlem42  46070  prpair  47375  ldepslinc  48238  sepnsepolem1  48601