Theorem rexralbidv 3220

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3061  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  freq1  5646  rexfiuz  15296  cau3lem  15303  caubnd2  15306  climi  15456  rlimi  15459  o1lo1  15483  2clim  15518  lo1le  15600  caucvgrlem  15621  caurcvgr  15622  caucvgb  15628  vdwlem10  16925  vdwlem13  16928  pmatcollpw2lem  22286  neiptopnei  22643  lmcvg  22773  lmss  22809  elpt  23083  elptr  23084  txlm  23159  tsmsi  23645  ustuqtop4  23756  isucn  23790  isucn2  23791  ucnima  23793  metcnpi  24060  metcnpi2  24061  metucn  24087  xrge0tsms  24357  elcncf  24412  cncfi  24417  lmmcvg  24785  lhop1  25538  ulmval  25899  ulmi  25905  ulmcaulem  25913  ulmdvlem3  25921  pntibnd  27103  pntlem3  27119  pntleml  27121  axtgcont1  27757  perpln1  27999  perpln2  28000  isperp  28001  brbtwn  28195  uvtx01vtx  28692  isgrpo  29788  ubthlem3  30163  ubth  30164  hcau  30475  hcaucvg  30477  hlimi  30479  hlimconvi  30482  hlim2  30483  elcnop  31148  elcnfn  31173  cnopc  31204  cnfnc  31221  lnopcon  31326  lnfncon  31347  riesz1  31356  xrge0tsmsd  32250  signsply0  33631  unblimceq0  35469  cvgcau  44280  limcleqr  44439  addlimc  44443  0ellimcdiv  44444  climd  44467  climisp  44541  lmbr3  44542  climrescn  44543  climxrrelem  44544  climxrre  44545  xlimpnfxnegmnf  44609  xlimxrre  44626  xlimmnf  44636  xlimpnf  44637  xlimmnfmpt  44638  xlimpnfmpt  44639  dfxlim2  44643  cncfshift  44669  cncfperiod  44674  ioodvbdlimc1lem1  44726  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  fourierdlem68  44969  fourierdlem87  44988  fourierdlem103  45004  fourierdlem104  45005  etransclem48  45077