Theorem 2ralbidv 3198

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem 2ralbidv

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3050

This theorem is referenced by:  3ralbidv  3201  6ralbidv  3203  cbvral3vw  3218  cbvral6vw  3220  cbvral3v  3338  rspc6v  3595  ralxpxfr2d  3598  poeq1  5533  soeq1  5551  isoeq1  7261  isoeq2  7262  isoeq3  7263  fnmpoovd  8027  xpord3inddlem  8094  smoeq  8280  xpf1o  9065  nqereu  10838  dedekind  11294  dedekindle  11295  seqcaopr2  13959  wrd2ind  14644  addcn2  15515  mulcn2  15517  mreexexd  17569  catlid  17604  catrid  17605  isfunc  17786  funcres2b  17819  isfull  17834  isfth  17838  fullres2c  17863  isnat  17872  evlfcl  18143  uncfcurf  18160  isprs  18217  isdrs  18222  ispos  18235  istos  18337  resspos  18350  resstos  18351  isdlat  18443  ismgmhm  18619  issubmgm  18625  sgrp1  18652  ismhm  18708  issubm  18726  sgrp2nmndlem4  18851  isnsg  19082  isghm  19142  isghmOLD  19143  isga  19218  pmtrdifwrdel  19412  sylow2blem2  19548  efglem  19643  efgi  19646  efgredlemb  19673  efgred  19675  frgpuplem  19699  iscmn  19716  isomnd  20050  ring1  20243  isirred  20353  rnghmval  20374  isrnghm  20375  isorng  20792  islmod  20813  lmodlema  20814  lssset  20882  islssd  20884  islmhm  20977  islmhm2  20988  isobs  21673  dmatel  22435  dmatmulcl  22442  scmateALT  22454  mdetunilem3  22556  mdetunilem4  22557  mdetunilem9  22562  cpmatel  22653  chpscmat  22784  hausnei2  23295  dfconn2  23361  llyeq  23412  nllyeq  23413  isucn2  24220  iducn  24224  ispsmet  24246  ismet  24265  isxmet  24266  metucn  24513  ngptgp  24578  nlmvscnlem1  24628  xmetdcn2  24780  addcnlem  24807  elcncf  24836  ipcnlem1  25199  cfili  25222  c1lip1  25956  aalioulem5  26298  aalioulem6  26299  aaliou  26300  aaliou2  26302  aaliou2b  26303  ulmcau  26358  ulmdvlem3  26365  cxpcn3lem  26711  mpodvdsmulf1o  27158  dvdsmulf1o  27160  chpdifbndlem2  27519  pntrsumbnd2  27532  addsprop  27946  negsprop  28004  istrkgb  28476  axtgsegcon  28485  axtg5seg  28486  axtgpasch  28488  axtgeucl  28493  iscgrg  28533  isismt  28555  isperp2  28736  f1otrg  28892  axcontlem10  28995  axcontlem12  28997  iscusgredg  29445  isgrpo  30521  isablo  30570  vacn  30718  smcnlem  30721  lnoval  30776  islno  30777  isphg  30841  ajmoi  30882  ajval  30885  adjmo  31856  elcnop  31881  ellnop  31882  elunop  31896  elhmop  31897  elcnfn  31906  ellnfn  31907  adjeu  31913  adjval  31914  adj1  31957  adjeq  31959  cnlnadjlem9  32099  cnlnadjeu  32102  cnlnssadj  32104  isst  32237  ishst  32238  cdj1i  32457  cdj3i  32465  ismnt  33014  mgcval  33018  isslmd  33233  slmdlema  33234  prmidlval  33467  isprmidl  33468  isrprm  33547  qqhucn  34098  ismntop  34132  axtgupdim2ALTV  34774  txpconn  35375  nn0prpw  36466  heicant  37795  equivbnd  37930  isismty  37941  heibor1lem  37949  iccbnd  37980  isass  37986  elghomlem1OLD  38025  elghomlem2OLD  38026  isrngohom  38105  iscom2  38135  pridlval  38173  ispridl  38174  isdmn3  38214  inecmo  38487  islfl  39259  isopos  39379  psubspset  39943  islaut  40282  ispautN  40298  ltrnset  40317  isltrn  40318  istrnN  40356  istendo  40959  sticksstones1  42339  sticksstones2  42340  sticksstones3  42341  sticksstones8  42346  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones15  42354  sn-isghm  42858  clsk1independent  44229  relpeq1  45127  relpeq2  45128  relpeq3  45129  sprsymrelfolem2  47681  sprsymrelfo  47685  reuopreuprim  47714  dmatALTbasel  48590  lindslinindsimp2  48651  lmod1  48680  isnrm4  49118  iscnrm4  49141  isuplem  49366  isthinc  49606  thincciso  49640  thinccisod  49641