Theorem 2ralbidv 3122

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  cbvral3vw  3387  cbvral3v  3390  ralxpxfr2d  3568  poeq1  5497  soeq1  5515  isoeq1  7168  isoeq2  7169  isoeq3  7170  fnmpoovd  7898  smoeq  8152  xpf1o  8875  nqereu  10616  dedekind  11068  dedekindle  11069  seqcaopr2  13687  wrd2ind  14364  addcn2  15231  mulcn2  15233  mreexexd  17274  catlid  17309  catrid  17310  isfunc  17495  funcres2b  17528  isfull  17542  isfth  17546  fullres2c  17571  isnat  17579  evlfcl  17856  uncfcurf  17873  isprs  17930  isdrs  17934  ispos  17947  istos  18051  isdlat  18155  sgrp1  18299  ismhm  18347  issubm  18357  sgrp2nmndlem4  18482  isnsg  18698  isghm  18749  isga  18812  pmtrdifwrdel  19008  sylow2blem2  19141  efglem  19237  efgi  19240  efgredlemb  19267  efgred  19269  frgpuplem  19293  iscmn  19309  ring1  19756  isirred  19856  islmod  20042  lmodlema  20043  lssset  20110  islssd  20112  islmhm  20204  islmhm2  20215  isobs  20837  dmatel  21550  dmatmulcl  21557  scmateALT  21569  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  cpmatel  21768  chpscmat  21899  hausnei2  22412  dfconn2  22478  llyeq  22529  nllyeq  22530  isucn2  23339  iducn  23343  ispsmet  23365  ismet  23384  isxmet  23385  metucn  23633  ngptgp  23698  nlmvscnlem1  23756  xmetdcn2  23906  addcnlem  23933  elcncf  23958  ipcnlem1  24314  cfili  24337  c1lip1  25066  aalioulem5  25401  aalioulem6  25402  aaliou  25403  aaliou2  25405  aaliou2b  25406  ulmcau  25459  ulmdvlem3  25466  cxpcn3lem  25805  dvdsmulf1o  26248  chpdifbndlem2  26607  pntrsumbnd2  26620  istrkgb  26720  axtgsegcon  26729  axtg5seg  26730  axtgpasch  26732  axtgeucl  26737  iscgrg  26777  isismt  26799  isperp2  26980  f1otrg  27136  axcontlem10  27244  axcontlem12  27246  iscusgredg  27693  isgrpo  28760  isablo  28809  vacn  28957  smcnlem  28960  lnoval  29015  islno  29016  isphg  29080  ajmoi  29121  ajval  29124  adjmo  30095  elcnop  30120  ellnop  30121  elunop  30135  elhmop  30136  elcnfn  30145  ellnfn  30146  adjeu  30152  adjval  30153  adj1  30196  adjeq  30198  cnlnadjlem9  30338  cnlnadjeu  30341  cnlnssadj  30343  isst  30476  ishst  30477  cdj1i  30696  cdj3i  30704  resspos  31146  resstos  31147  ismnt  31163  mgcval  31167  isomnd  31229  isslmd  31357  slmdlema  31358  isorng  31400  prmidlval  31514  isprmidl  31515  isrprm  31567  qqhucn  31842  ismntop  31876  axtgupdim2ALTV  32548  txpconn  33094  xpord3ind  33727  nn0prpw  34439  heicant  35739  equivbnd  35875  isismty  35886  heibor1lem  35894  iccbnd  35925  isass  35931  elghomlem1OLD  35970  elghomlem2OLD  35971  isrngohom  36050  iscom2  36080  pridlval  36118  ispridl  36119  isdmn3  36159  inecmo  36414  islfl  37001  isopos  37121  psubspset  37685  islaut  38024  ispautN  38040  ltrnset  38059  isltrn  38060  istrnN  38098  istendo  38701  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones8  40037  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones15  40045  clsk1independent  41545  sprsymrelfolem2  44833  sprsymrelfo  44837  reuopreuprim  44866  ismgmhm  45225  issubmgm  45231  rnghmval  45337  isrnghm  45338  lidlmsgrp  45372  lidlrng  45373  dmatALTbasel  45631  lindslinindsimp2  45692  lmod1  45721  isnrm4  46112  iscnrm4  46136  isthinc  46190  thincciso  46218