Theorem 2ralbidv 3209

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3052

This theorem is referenced by:  3ralbidv  3212  6ralbidv  3214  cbvral3vw  3231  cbvral6vw  3233  cbvral3v  3354  rspc6v  3628  ralxpxfr2d  3631  poeq1  5597  soeq1  5615  isoeq1  7329  isoeq2  7330  isoeq3  7331  fnmpoovd  8101  xpord3inddlem  8168  smoeq  8380  xpf1o  9177  nqereu  10972  dedekind  11427  dedekindle  11428  seqcaopr2  14058  wrd2ind  14731  addcn2  15596  mulcn2  15598  mreexexd  17661  catlid  17696  catrid  17697  isfunc  17883  funcres2b  17916  isfull  17932  isfth  17936  fullres2c  17961  isnat  17970  evlfcl  18247  uncfcurf  18264  isprs  18322  isdrs  18326  ispos  18339  istos  18443  isdlat  18547  ismgmhm  18689  issubmgm  18695  sgrp1  18722  ismhm  18775  issubm  18793  sgrp2nmndlem4  18918  isnsg  19149  isghm  19209  isghmOLD  19210  isga  19285  pmtrdifwrdel  19483  sylow2blem2  19619  efglem  19714  efgi  19717  efgredlemb  19744  efgred  19746  frgpuplem  19770  iscmn  19787  ring1  20289  isirred  20401  rnghmval  20422  isrnghm  20423  islmod  20840  lmodlema  20841  lssset  20910  islssd  20912  islmhm  21005  islmhm2  21016  isobs  21718  dmatel  22486  dmatmulcl  22493  scmateALT  22505  mdetunilem3  22607  mdetunilem4  22608  mdetunilem9  22613  cpmatel  22704  chpscmat  22835  hausnei2  23348  dfconn2  23414  llyeq  23465  nllyeq  23466  isucn2  24275  iducn  24279  ispsmet  24301  ismet  24320  isxmet  24321  metucn  24571  ngptgp  24636  nlmvscnlem1  24694  xmetdcn2  24844  addcnlem  24871  elcncf  24900  ipcnlem1  25264  cfili  25287  c1lip1  26021  aalioulem5  26364  aalioulem6  26365  aaliou  26366  aaliou2  26368  aaliou2b  26369  ulmcau  26424  ulmdvlem3  26431  cxpcn3lem  26775  mpodvdsmulf1o  27222  dvdsmulf1o  27224  chpdifbndlem2  27583  pntrsumbnd2  27596  addsprop  27990  negsprop  28044  istrkgb  28382  axtgsegcon  28391  axtg5seg  28392  axtgpasch  28394  axtgeucl  28399  iscgrg  28439  isismt  28461  isperp2  28642  f1otrg  28798  axcontlem10  28907  axcontlem12  28909  iscusgredg  29359  isgrpo  30430  isablo  30479  vacn  30627  smcnlem  30630  lnoval  30685  islno  30686  isphg  30750  ajmoi  30791  ajval  30794  adjmo  31765  elcnop  31790  ellnop  31791  elunop  31805  elhmop  31806  elcnfn  31815  ellnfn  31816  adjeu  31822  adjval  31823  adj1  31866  adjeq  31868  cnlnadjlem9  32008  cnlnadjeu  32011  cnlnssadj  32013  isst  32146  ishst  32147  cdj1i  32366  cdj3i  32374  resspos  32836  resstos  32837  ismnt  32853  mgcval  32857  isomnd  32936  isslmd  33066  slmdlema  33067  isorng  33177  prmidlval  33312  isprmidl  33313  isrprm  33392  qqhucn  33807  ismntop  33841  axtgupdim2ALTV  34514  txpconn  35060  nn0prpw  36035  heicant  37356  equivbnd  37491  isismty  37502  heibor1lem  37510  iccbnd  37541  isass  37547  elghomlem1OLD  37586  elghomlem2OLD  37587  isrngohom  37666  iscom2  37696  pridlval  37734  ispridl  37735  isdmn3  37775  inecmo  38053  islfl  38758  isopos  38878  psubspset  39443  islaut  39782  ispautN  39798  ltrnset  39817  isltrn  39818  istrnN  39856  istendo  40459  sticksstones1  41844  sticksstones2  41845  sticksstones3  41846  sticksstones8  41851  sticksstones10  41853  sticksstones11  41854  sticksstones12a  41855  sticksstones15  41859  sn-isghm  42327  clsk1independent  43713  sprsymrelfolem2  47065  sprsymrelfo  47069  reuopreuprim  47098  dmatALTbasel  47785  lindslinindsimp2  47846  lmod1  47875  isnrm4  48264  iscnrm4  48288  isthinc  48342  thincciso  48370