Theorem 2ralbidv 3218

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  3ralbidv  3221  6ralbidv  3223  cbvral3vw  3240  cbvral6vw  3242  cbvral3v  3367  rspc6v  3642  ralxpxfr2d  3645  poeq1  5599  soeq1  5617  isoeq1  7336  isoeq2  7337  isoeq3  7338  fnmpoovd  8110  xpord3inddlem  8177  smoeq  8388  xpf1o  9177  nqereu  10966  dedekind  11421  dedekindle  11422  seqcaopr2  14075  wrd2ind  14757  addcn2  15626  mulcn2  15628  mreexexd  17692  catlid  17727  catrid  17728  isfunc  17914  funcres2b  17947  isfull  17963  isfth  17967  fullres2c  17992  isnat  18001  evlfcl  18278  uncfcurf  18295  isprs  18353  isdrs  18358  ispos  18371  istos  18475  isdlat  18579  ismgmhm  18721  issubmgm  18727  sgrp1  18754  ismhm  18810  issubm  18828  sgrp2nmndlem4  18953  isnsg  19185  isghm  19245  isghmOLD  19246  isga  19321  pmtrdifwrdel  19517  sylow2blem2  19653  efglem  19748  efgi  19751  efgredlemb  19778  efgred  19780  frgpuplem  19804  iscmn  19821  ring1  20323  isirred  20435  rnghmval  20456  isrnghm  20457  islmod  20878  lmodlema  20879  lssset  20948  islssd  20950  islmhm  21043  islmhm2  21054  isobs  21757  dmatel  22514  dmatmulcl  22521  scmateALT  22533  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  cpmatel  22732  chpscmat  22863  hausnei2  23376  dfconn2  23442  llyeq  23493  nllyeq  23494  isucn2  24303  iducn  24307  ispsmet  24329  ismet  24348  isxmet  24349  metucn  24599  ngptgp  24664  nlmvscnlem1  24722  xmetdcn2  24872  addcnlem  24899  elcncf  24928  ipcnlem1  25292  cfili  25315  c1lip1  26050  aalioulem5  26392  aalioulem6  26393  aaliou  26394  aaliou2  26396  aaliou2b  26397  ulmcau  26452  ulmdvlem3  26459  cxpcn3lem  26804  mpodvdsmulf1o  27251  dvdsmulf1o  27253  chpdifbndlem2  27612  pntrsumbnd2  27625  addsprop  28023  negsprop  28081  istrkgb  28477  axtgsegcon  28486  axtg5seg  28487  axtgpasch  28489  axtgeucl  28494  iscgrg  28534  isismt  28556  isperp2  28737  f1otrg  28893  axcontlem10  29002  axcontlem12  29004  iscusgredg  29454  isgrpo  30525  isablo  30574  vacn  30722  smcnlem  30725  lnoval  30780  islno  30781  isphg  30845  ajmoi  30886  ajval  30889  adjmo  31860  elcnop  31885  ellnop  31886  elunop  31900  elhmop  31901  elcnfn  31910  ellnfn  31911  adjeu  31917  adjval  31918  adj1  31961  adjeq  31963  cnlnadjlem9  32103  cnlnadjeu  32106  cnlnssadj  32108  isst  32241  ishst  32242  cdj1i  32461  cdj3i  32469  resspos  32940  resstos  32941  ismnt  32957  mgcval  32961  isomnd  33060  isslmd  33190  slmdlema  33191  isorng  33308  prmidlval  33444  isprmidl  33445  isrprm  33524  qqhucn  33954  ismntop  33988  axtgupdim2ALTV  34661  txpconn  35216  nn0prpw  36305  heicant  37641  equivbnd  37776  isismty  37787  heibor1lem  37795  iccbnd  37826  isass  37832  elghomlem1OLD  37871  elghomlem2OLD  37872  isrngohom  37951  iscom2  37981  pridlval  38019  ispridl  38020  isdmn3  38060  inecmo  38336  islfl  39041  isopos  39161  psubspset  39726  islaut  40065  ispautN  40081  ltrnset  40100  isltrn  40101  istrnN  40139  istendo  40742  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones15  42142  sn-isghm  42659  clsk1independent  44035  sprsymrelfolem2  47417  sprsymrelfo  47421  reuopreuprim  47450  dmatALTbasel  48247  lindslinindsimp2  48308  lmod1  48337  isnrm4  48726  iscnrm4  48750  isthinc  48820  thincciso  48848  thinccisod  48849