Theorem 2ralbidv 3196

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

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

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 3048

This theorem is referenced by:  3ralbidv  3199  6ralbidv  3201  cbvral3vw  3216  cbvral6vw  3218  cbvral3v  3336  rspc6v  3593  ralxpxfr2d  3596  poeq1  5525  soeq1  5543  isoeq1  7251  isoeq2  7252  isoeq3  7253  fnmpoovd  8017  xpord3inddlem  8084  smoeq  8270  xpf1o  9052  nqereu  10820  dedekind  11276  dedekindle  11277  seqcaopr2  13945  wrd2ind  14630  addcn2  15501  mulcn2  15503  mreexexd  17554  catlid  17589  catrid  17590  isfunc  17771  funcres2b  17804  isfull  17819  isfth  17823  fullres2c  17848  isnat  17857  evlfcl  18128  uncfcurf  18145  isprs  18202  isdrs  18207  ispos  18220  istos  18322  resspos  18335  resstos  18336  isdlat  18428  ismgmhm  18604  issubmgm  18610  sgrp1  18637  ismhm  18693  issubm  18711  sgrp2nmndlem4  18836  isnsg  19067  isghm  19127  isghmOLD  19128  isga  19203  pmtrdifwrdel  19397  sylow2blem2  19533  efglem  19628  efgi  19631  efgredlemb  19658  efgred  19660  frgpuplem  19684  iscmn  19701  isomnd  20035  ring1  20228  isirred  20337  rnghmval  20358  isrnghm  20359  isorng  20776  islmod  20797  lmodlema  20798  lssset  20866  islssd  20868  islmhm  20961  islmhm2  20972  isobs  21657  dmatel  22408  dmatmulcl  22415  scmateALT  22427  mdetunilem3  22529  mdetunilem4  22530  mdetunilem9  22535  cpmatel  22626  chpscmat  22757  hausnei2  23268  dfconn2  23334  llyeq  23385  nllyeq  23386  isucn2  24193  iducn  24197  ispsmet  24219  ismet  24238  isxmet  24239  metucn  24486  ngptgp  24551  nlmvscnlem1  24601  xmetdcn2  24753  addcnlem  24780  elcncf  24809  ipcnlem1  25172  cfili  25195  c1lip1  25929  aalioulem5  26271  aalioulem6  26272  aaliou  26273  aaliou2  26275  aaliou2b  26276  ulmcau  26331  ulmdvlem3  26338  cxpcn3lem  26684  mpodvdsmulf1o  27131  dvdsmulf1o  27133  chpdifbndlem2  27492  pntrsumbnd2  27505  addsprop  27919  negsprop  27977  istrkgb  28433  axtgsegcon  28442  axtg5seg  28443  axtgpasch  28445  axtgeucl  28450  iscgrg  28490  isismt  28512  isperp2  28693  f1otrg  28849  axcontlem10  28951  axcontlem12  28953  iscusgredg  29401  isgrpo  30477  isablo  30526  vacn  30674  smcnlem  30677  lnoval  30732  islno  30733  isphg  30797  ajmoi  30838  ajval  30841  adjmo  31812  elcnop  31837  ellnop  31838  elunop  31852  elhmop  31853  elcnfn  31862  ellnfn  31863  adjeu  31869  adjval  31870  adj1  31913  adjeq  31915  cnlnadjlem9  32055  cnlnadjeu  32058  cnlnssadj  32060  isst  32193  ishst  32194  cdj1i  32413  cdj3i  32421  ismnt  32964  mgcval  32968  isslmd  33171  slmdlema  33172  prmidlval  33402  isprmidl  33403  isrprm  33482  qqhucn  34005  ismntop  34039  axtgupdim2ALTV  34681  txpconn  35276  nn0prpw  36367  heicant  37705  equivbnd  37840  isismty  37851  heibor1lem  37859  iccbnd  37890  isass  37896  elghomlem1OLD  37935  elghomlem2OLD  37936  isrngohom  38015  iscom2  38045  pridlval  38083  ispridl  38084  isdmn3  38124  inecmo  38397  islfl  39169  isopos  39289  psubspset  39853  islaut  40192  ispautN  40208  ltrnset  40227  isltrn  40228  istrnN  40266  istendo  40869  sticksstones1  42249  sticksstones2  42250  sticksstones3  42251  sticksstones8  42256  sticksstones10  42258  sticksstones11  42259  sticksstones12a  42260  sticksstones15  42264  sn-isghm  42776  clsk1independent  44149  relpeq1  45047  relpeq2  45048  relpeq3  45049  sprsymrelfolem2  47603  sprsymrelfo  47607  reuopreuprim  47636  dmatALTbasel  48513  lindslinindsimp2  48574  lmod1  48603  isnrm4  49041  iscnrm4  49064  isuplem  49290  isthinc  49530  thincciso  49564  thinccisod  49565