Theorem 2ralbidv 3228

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  3ralbidv  3231  6ralbidv  3233  cbvral3vw  3248  cbvral6vw  3250  cbvral3v  3359  rspc6v  3604  ralxpxfr2d  3607  poeq1  5560  soeq1  5578  isoeq1  7303  isoeq2  7304  isoeq3  7305  fnmpoovd  8068  xpord3inddlem  8136  smoeq  8323  xpf1o  9113  nqereu  10889  dedekind  11348  dedekindle  11349  seqcaopr2  14053  wrd2ind  14738  addcn2  15623  mulcn2  15625  mreexexd  17682  catlid  17717  catrid  17718  isfunc  17899  funcres2b  17932  isfull  17947  isfth  17951  fullres2c  17976  isnat  17985  evlfcl  18256  uncfcurf  18273  isprs  18330  isdrs  18335  ispos  18348  istos  18450  resspos  18463  resstos  18464  isdlat  18556  ismgmhm  18732  issubmgm  18738  sgrp1  18765  ismhm  18821  issubm  18839  sgrp2nmndlem4  18967  isnsg  19198  isghm  19258  isga  19333  pmtrdifwrdel  19527  sylow2blem2  19663  efglem  19758  efgi  19761  efgredlemb  19788  efgred  19790  frgpuplem  19814  iscmn  19831  isomnd  20165  ring1  20362  isirred  20470  rnghmval  20491  isrnghm  20492  isorng  20912  islmod  20933  lmodlema  20934  lssset  21002  islssd  21004  islmhm  21096  islmhm2  21107  isobs  21774  dmatel  22555  dmatmulcl  22562  scmateALT  22574  mdetunilem3  22676  mdetunilem4  22677  mdetunilem9  22682  cpmatel  22773  chpscmat  22904  hausnei2  23415  dfconn2  23481  llyeq  23532  nllyeq  23533  isucn2  24340  iducn  24344  ispsmet  24366  ismet  24385  isxmet  24386  metucn  24633  ngptgp  24698  nlmvscnlem1  24748  xmetdcn2  24900  addcnlem  24927  elcncf  24953  ipcnlem1  25309  cfili  25332  c1lip1  26061  aalioulem5  26402  aalioulem6  26403  aaliou  26404  aaliou2  26406  aaliou2b  26407  ulmcau  26460  ulmdvlem3  26467  cxpcn3lem  26814  mpodvdsmulf1o  27260  dvdsmulf1o  27262  chpdifbndlem2  27620  pntrsumbnd2  27633  addsprop  28071  negsprop  28130  istrkgb  28626  axtgsegcon  28635  axtg5seg  28636  axtgpasch  28638  axtgeucl  28643  iscgrg  28683  isismt  28705  isperp2  28890  f1otrg  29073  axcontlem10  29176  axcontlem12  29178  iscusgredg  29626  isgrpo  30702  isablo  30751  vacn  30899  smcnlem  30902  lnoval  30957  islno  30958  isphg  31022  ajmoi  31063  ajval  31066  adjmo  32037  elcnop  32062  ellnop  32063  elunop  32077  elhmop  32078  elcnfn  32087  ellnfn  32088  adjeu  32094  adjval  32095  adj1  32138  adjeq  32140  cnlnadjlem9  32280  cnlnadjeu  32283  cnlnssadj  32285  isst  32418  ishst  32419  cdj1i  32638  cdj3i  32646  ismnt  33163  mgcval  33167  isslmd  33384  slmdlema  33385  prmidlval  33625  isprmidl  33626  isrprm  33715  qqhucn  34291  ismntop  34325  axtgupdim2ALTV  34964  txpconn  35587  nmulprop  36545  nmulr0  36550  nn0prpw  36688  heicant  38159  equivbnd  38294  isismty  38305  heibor1lem  38313  iccbnd  38344  isass  38350  elghomlem1OLD  38389  elghomlem2OLD  38390  isrngohom  38469  iscom2  38499  pridlval  38537  ispridl  38538  isdmn3  38578  inecmo  38859  islfl  39689  isopos  39809  psubspset  40373  islaut  40712  ispautN  40728  ltrnset  40747  isltrn  40748  istrnN  40786  istendo  41389  sticksstones1  42768  sticksstones2  42769  sticksstones3  42770  sticksstones8  42775  sticksstones10  42777  sticksstones11  42778  sticksstones12a  42779  sticksstones15  42783  sn-isghm  43260  clsk1independent  44627  relpeq1  45525  relpeq2  45526  relpeq3  45527  sprsymrelfolem2  48104  sprsymrelfo  48108  reuopreuprim  48137  dmatALTbasel  49029  lindslinindsimp2  49090  lmod1  49119  isnrm4  49557  iscnrm4  49580  isuplem  49805  isthinc  50045  thincciso  50079  thinccisod  50080