Theorem 2ralbidv 3201

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

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

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 1912

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

This theorem is referenced by:  3ralbidv  3204  6ralbidv  3206  cbvral3vw  3221  cbvral6vw  3223  cbvral3v  3341  rspc6v  3598  ralxpxfr2d  3601  poeq1  5536  soeq1  5554  isoeq1  7265  isoeq2  7266  isoeq3  7267  fnmpoovd  8031  xpord3inddlem  8098  smoeq  8284  xpf1o  9071  nqereu  10844  dedekind  11300  dedekindle  11301  seqcaopr2  13965  wrd2ind  14650  addcn2  15521  mulcn2  15523  mreexexd  17575  catlid  17610  catrid  17611  isfunc  17792  funcres2b  17825  isfull  17840  isfth  17844  fullres2c  17869  isnat  17878  evlfcl  18149  uncfcurf  18166  isprs  18223  isdrs  18228  ispos  18241  istos  18343  resspos  18356  resstos  18357  isdlat  18449  ismgmhm  18625  issubmgm  18631  sgrp1  18658  ismhm  18714  issubm  18732  sgrp2nmndlem4  18857  isnsg  19088  isghm  19148  isghmOLD  19149  isga  19224  pmtrdifwrdel  19418  sylow2blem2  19554  efglem  19649  efgi  19652  efgredlemb  19679  efgred  19681  frgpuplem  19705  iscmn  19722  isomnd  20056  ring1  20249  isirred  20359  rnghmval  20380  isrnghm  20381  isorng  20798  islmod  20819  lmodlema  20820  lssset  20888  islssd  20890  islmhm  20983  islmhm2  20994  isobs  21679  dmatel  22441  dmatmulcl  22448  scmateALT  22460  mdetunilem3  22562  mdetunilem4  22563  mdetunilem9  22568  cpmatel  22659  chpscmat  22790  hausnei2  23301  dfconn2  23367  llyeq  23418  nllyeq  23419  isucn2  24226  iducn  24230  ispsmet  24252  ismet  24271  isxmet  24272  metucn  24519  ngptgp  24584  nlmvscnlem1  24634  xmetdcn2  24786  addcnlem  24813  elcncf  24842  ipcnlem1  25205  cfili  25228  c1lip1  25962  aalioulem5  26304  aalioulem6  26305  aaliou  26306  aaliou2  26308  aaliou2b  26309  ulmcau  26364  ulmdvlem3  26371  cxpcn3lem  26717  mpodvdsmulf1o  27164  dvdsmulf1o  27166  chpdifbndlem2  27525  pntrsumbnd2  27538  addsprop  27976  negsprop  28035  istrkgb  28531  axtgsegcon  28540  axtg5seg  28541  axtgpasch  28543  axtgeucl  28548  iscgrg  28588  isismt  28610  isperp2  28791  f1otrg  28947  axcontlem10  29050  axcontlem12  29052  iscusgredg  29500  isgrpo  30576  isablo  30625  vacn  30773  smcnlem  30776  lnoval  30831  islno  30832  isphg  30896  ajmoi  30937  ajval  30940  adjmo  31911  elcnop  31936  ellnop  31937  elunop  31951  elhmop  31952  elcnfn  31961  ellnfn  31962  adjeu  31968  adjval  31969  adj1  32012  adjeq  32014  cnlnadjlem9  32154  cnlnadjeu  32157  cnlnssadj  32159  isst  32292  ishst  32293  cdj1i  32512  cdj3i  32520  ismnt  33067  mgcval  33071  isslmd  33286  slmdlema  33287  prmidlval  33520  isprmidl  33521  isrprm  33600  qqhucn  34151  ismntop  34185  axtgupdim2ALTV  34827  txpconn  35428  nn0prpw  36519  heicant  37858  equivbnd  37993  isismty  38004  heibor1lem  38012  iccbnd  38043  isass  38049  elghomlem1OLD  38088  elghomlem2OLD  38089  isrngohom  38168  iscom2  38198  pridlval  38236  ispridl  38237  isdmn3  38277  inecmo  38558  islfl  39388  isopos  39508  psubspset  40072  islaut  40411  ispautN  40427  ltrnset  40446  isltrn  40447  istrnN  40485  istendo  41088  sticksstones1  42468  sticksstones2  42469  sticksstones3  42470  sticksstones8  42475  sticksstones10  42477  sticksstones11  42478  sticksstones12a  42479  sticksstones15  42483  sn-isghm  42983  clsk1independent  44354  relpeq1  45252  relpeq2  45253  relpeq3  45254  sprsymrelfolem2  47806  sprsymrelfo  47810  reuopreuprim  47839  dmatALTbasel  48715  lindslinindsimp2  48776  lmod1  48805  isnrm4  49243  iscnrm4  49266  isuplem  49491  isthinc  49731  thincciso  49765  thinccisod  49766