Theorem 2rexbii 3109

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

Syntax hints:   ↔ wb 206  ∃wrex 3053

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 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexnal3  3116  3reeanv  3210  2nreu  4407  poxp2  8122  poxp3  8129  poseq  8137  1sdom  9195  ttrcltr  9669  addcompr  10974  mulcompr  10976  4fvwrd4  13609  ntrivcvgmul  15868  prodmo  15902  pythagtriplem2  16788  pythagtrip  16805  cat1  18059  isnsgrp  18650  efgrelexlemb  19680  ordthaus  23271  regr1lem2  23627  fmucndlem  24178  madeval2  27761  zaddscl  28282  zmulscld  28285  dfcgra2  28757  axpasch  28868  axeuclid  28890  axcontlem4  28894  umgr2edg1  29138  wwlksnwwlksnon  29845  xrofsup  32690  constrcbvlem  33745  satfvsucsuc  35352  satf0  35359  altopelaltxp  35964  brsegle  36096  fimgmcyclem  42521  fimgmcyc  42522  mzpcompact2lem  42739  sbc4rex  42777  7rexfrabdioph  42788  expdiophlem1  43010  fourierdlem42  46147  prpair  47502  ldepslinc  48498  sepnsepolem1  48910