Theorem 2ralbidv 3230

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  3ralbidv  3233  6ralbidv  3235  cbvral3vw  3250  cbvral6vw  3252  cbvral3v  3359  rspc6v  3600  ralxpxfr2d  3603  poeq1  5566  soeq1  5584  isoeq1  7335  isoeq2  7336  isoeq3  7337  fnmpoovd  8109  xpord3inddlem  8184  smoeq  8372  xpf1o  9172  nqereu  11027  dedekind  11486  dedekindle  11487  seqcaopr2  14194  wrd2ind  14886  addcn2  15776  mulcn2  15778  mreexexd  17837  catlid  17872  catrid  17873  isfunc  18054  funcres2b  18087  isfull  18102  isfth  18106  fullres2c  18131  isnat  18140  evlfcl  18411  uncfcurf  18428  isprs  18485  isdrs  18490  ispos  18503  istos  18605  resspos  18618  resstos  18619  isdlat  18711  ismgmhm  18900  issubmgm  18906  sgrp1  18933  ismhm  18995  issubm  19013  sgrp2nmndlem4  19142  isnsg  19380  isghm  19445  isga  19520  pmtrdifwrdel  19714  sylow2blem2  19850  efglem  19945  efgi  19948  efgredlemb  19975  efgred  19977  frgpuplem  20001  iscmn  20018  isomnd  20352  ring1  20556  isirred  20664  rnghmval  20685  isrnghm  20686  rhmval0  20720  isrhm0  20721  isorng  21133  islmod  21154  lmodlema  21155  lssset  21223  islssd  21225  islmhm  21317  islmhm2  21328  prmidlval  21633  isprmidl  21634  isobs  22041  dmatel  22823  dmatmulcl  22830  scmateALT  22842  mdetunilem3  22944  mdetunilem4  22945  mdetunilem9  22950  cpmatel  23044  chpscmat  23175  hausnei2  23686  dfconn2  23752  llyeq  23804  nllyeq  23805  isucn2  24612  iducn  24616  ispsmet  24638  ismet  24657  isxmet  24658  metucn  24905  ngptgp  24970  nlmvscnlem1  25020  xmetdcn2  25172  addcnlem  25199  elcncf  25225  ipcnlem1  25581  cfili  25604  c1lip1  26332  aalioulem5  26678  aalioulem6  26679  aaliou  26680  aaliou2  26682  aaliou2b  26683  ulmcau  26737  ulmdvlem3  26744  cxpcn3lem  27090  mpodvdsmulf1o  27536  dvdsmulf1o  27538  chpdifbndlem2  27896  pntrsumbnd2  27909  addsprop  28377  negsprop  28436  istrkgb  28932  axtgsegcon  28941  axtg5seg  28942  axtgpasch  28944  axtgeucl  28949  iscgrg  28990  isismt  29012  isperp2  29205  f1otrg  29463  axcontlem10  29566  axcontlem12  29568  iscusgredg  30019  isgrpo  31114  isablo  31163  vacn  31311  smcnlem  31314  lnoval  31369  islno  31370  isphg  31434  ajmoi  31475  ajval  31478  adjmo  32449  elcnop  32474  ellnop  32475  elunop  32489  elhmop  32490  elcnfn  32499  ellnfn  32500  adjeu  32506  adjval  32507  adj1  32550  adjeq  32552  cnlnadjlem9  32692  cnlnadjeu  32695  cnlnssadj  32697  isst  32830  ishst  32831  cdj1i  33050  cdj3i  33058  ismnt  33600  mgcval  33604  isslmd  33819  slmdlema  33820  isrprm  34105  qqhucn  34680  ismntop  34714  axtgupdim2ALTV  35353  txpconn  36121  nmulprop  37072  nmulr0  37077  nmuladdel  37094  ltnmul  37098  nn0prpw  37244  heicant  38719  equivbnd  38870  isismty  38881  heibor1lem  38889  iccbnd  38920  isass  38926  elghomlem1OLD  38965  elghomlem2OLD  38966  isrngohom  39045  iscom2  39075  pridlval  39113  ispridl  39114  isdmn3  39154  inecmo  39433  islfl  40263  isopos  40383  psubspset  40947  islaut  41286  ispautN  41302  ltrnset  41321  isltrn  41322  istrnN  41360  istendo  41963  sticksstones1  43342  sticksstones2  43343  sticksstones3  43344  sticksstones8  43349  sticksstones10  43351  sticksstones11  43352  sticksstones12a  43353  sticksstones15  43357  sn-isghm  43830  clsk1independent  45192  relpeq1  46079  relpeq2  46080  relpeq3  46081  sprsymrelfolem2  48720  sprsymrelfo  48724  reuopreuprim  48753  isidom3  49587  dmatALTbasel  49659  lindslinindsimp2  49720  lmod1  49749  isnrm4  50190  iscnrm4  50213  isuplem  50440  fucoisfunc2lem1  50633  isthinc  50699  thincciso  50733  thinccisod  50734