Theorem 2ralbidv 3231

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  3ralbidv  3234  6ralbidv  3236  cbvral3vw  3251  cbvral6vw  3253  cbvral3v  3361  rspc6v  3604  ralxpxfr2d  3607  poeq1  5574  soeq1  5592  isoeq1  7324  isoeq2  7325  isoeq3  7326  fnmpoovd  8088  xpord3inddlem  8156  smoeq  8343  xpf1o  9134  nqereu  10933  dedekind  11392  dedekindle  11393  seqcaopr2  14096  wrd2ind  14786  addcn2  15673  mulcn2  15675  mreexexd  17730  catlid  17765  catrid  17766  isfunc  17947  funcres2b  17980  isfull  17995  isfth  17999  fullres2c  18024  isnat  18033  evlfcl  18304  uncfcurf  18321  isprs  18378  isdrs  18383  ispos  18396  istos  18498  resspos  18511  resstos  18512  isdlat  18604  ismgmhm  18790  issubmgm  18796  sgrp1  18823  ismhm  18884  issubm  18902  sgrp2nmndlem4  19031  isnsg  19269  isghm  19334  isga  19409  pmtrdifwrdel  19603  sylow2blem2  19739  efglem  19834  efgi  19837  efgredlemb  19864  efgred  19866  frgpuplem  19890  iscmn  19907  isomnd  20241  ring1  20443  isirred  20551  rnghmval  20572  isrnghm  20573  rhmval0  20607  isrhm0  20608  isorng  21018  islmod  21039  lmodlema  21040  lssset  21108  islssd  21110  islmhm  21202  islmhm2  21213  prmidlval  21516  isprmidl  21517  isobs  21924  dmatel  22704  dmatmulcl  22711  scmateALT  22723  mdetunilem3  22825  mdetunilem4  22826  mdetunilem9  22831  cpmatel  22922  chpscmat  23053  hausnei2  23564  dfconn2  23630  llyeq  23682  nllyeq  23683  isucn2  24490  iducn  24494  ispsmet  24516  ismet  24535  isxmet  24536  metucn  24783  ngptgp  24848  nlmvscnlem1  24898  xmetdcn2  25050  addcnlem  25077  elcncf  25103  ipcnlem1  25459  cfili  25482  c1lip1  26211  aalioulem5  26554  aalioulem6  26555  aaliou  26556  aaliou2  26558  aaliou2b  26559  ulmcau  26613  ulmdvlem3  26620  cxpcn3lem  26967  mpodvdsmulf1o  27413  dvdsmulf1o  27415  chpdifbndlem2  27773  pntrsumbnd2  27786  addsprop  28224  negsprop  28283  istrkgb  28779  axtgsegcon  28788  axtg5seg  28789  axtgpasch  28791  axtgeucl  28796  iscgrg  28836  isismt  28858  isperp2  29050  f1otrg  29279  axcontlem10  29382  axcontlem12  29384  iscusgredg  29835  isgrpo  30924  isablo  30973  vacn  31121  smcnlem  31124  lnoval  31179  islno  31180  isphg  31244  ajmoi  31285  ajval  31288  adjmo  32259  elcnop  32284  ellnop  32285  elunop  32299  elhmop  32300  elcnfn  32309  ellnfn  32310  adjeu  32316  adjval  32317  adj1  32360  adjeq  32362  cnlnadjlem9  32502  cnlnadjeu  32505  cnlnssadj  32507  isst  32640  ishst  32641  cdj1i  32860  cdj3i  32868  ismnt  33371  mgcval  33375  isslmd  33590  slmdlema  33591  isrprm  33875  qqhucn  34450  ismntop  34484  axtgupdim2ALTV  35124  txpconn  35765  nmulprop  36723  nmulr0  36728  nmuladdel  36745  ltnmul  36749  nn0prpw  36895  heicant  38367  equivbnd  38503  isismty  38514  heibor1lem  38522  iccbnd  38553  isass  38559  elghomlem1OLD  38598  elghomlem2OLD  38599  isrngohom  38678  iscom2  38708  pridlval  38746  ispridl  38747  isdmn3  38787  inecmo  39066  islfl  39896  isopos  40016  psubspset  40580  islaut  40919  ispautN  40935  ltrnset  40954  isltrn  40955  istrnN  40993  istendo  41596  sticksstones1  42975  sticksstones2  42976  sticksstones3  42977  sticksstones8  42982  sticksstones10  42984  sticksstones11  42985  sticksstones12a  42986  sticksstones15  42990  sn-isghm  43482  clsk1independent  44849  relpeq1  45730  relpeq2  45731  relpeq3  45732  sprsymrelfolem2  48319  sprsymrelfo  48323  reuopreuprim  48352  isidom3  49186  dmatALTbasel  49258  lindslinindsimp2  49319  lmod1  49348  isnrm4  49785  iscnrm4  49808  isuplem  50033  isthinc  50273  thincciso  50307  thinccisod  50308