Theorem rexralbidv 3232

Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexralbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥, 𝑦)   𝜒(𝑥, 𝑦)   𝐴(𝑥, 𝑦)   𝐵(𝑥, 𝑦)

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 3189	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3190	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  freq1  5625  rexfiuz  15559  cau3lem  15566  caubnd2  15569  climi  15721  rlimi  15724  o1lo1  15748  2clim  15783  lo1le  15863  caucvgrlem  15884  caurcvgr  15885  caucvgb  15891  vdwlem10  17212  vdwlem13  17215  pmatcollpw2lem  23150  neiptopnei  23505  lmcvg  23635  lmss  23671  elpt  23946  elptr  23947  txlm  24022  tsmsi  24508  ustuqtop4  24618  isucn  24651  isucn2  24652  ucnima  24654  metcnpi  24918  metcnpi2  24919  metucn  24945  xrge0tsms  25209  elcncf  25265  cncfi  25270  lmmcvg  25637  lhop1  26389  ulmval  26764  ulmi  26770  ulmcaulem  26778  ulmdvlem3  26786  pntibnd  27977  pntlem3  27993  pntleml  27995  axtgcont1  28987  perpln1  29242  perpln2  29243  isperp  29244  brbtwn  29534  uvtx01vtx  30035  isgrpo  31156  ubthlem3  31531  ubth  31532  hcau  31843  hcaucvg  31845  hlimi  31847  hlimconvi  31850  hlim2  31851  elcnop  32516  elcnfn  32541  cnopc  32572  cnfnc  32589  lnopcon  32694  lnfncon  32715  riesz1  32724  xrge0tsmsd  33733  signsply0  35291  srepdf  36128  unblimceq0  37588  cvgcau  46773  limcleqr  46927  addlimc  46931  0ellimcdiv  46932  climd  46955  climisp  47029  lmbr3  47030  climrescn  47031  climxrrelem  47032  climxrre  47033  xlimpnfxnegmnf  47097  xlimxrre  47114  xlimmnf  47124  xlimpnf  47125  xlimmnfmpt  47126  xlimpnfmpt  47127  dfxlim2  47131  cncfshift  47157  cncfperiod  47162  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  fourierdlem68  47457  fourierdlem87  47476  fourierdlem103  47492  fourierdlem104  47493  etransclem48  47565