Theorem 2ralbidv 3201

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  3ralbidv  3204  6ralbidv  3206  cbvral3vw  3221  cbvral6vw  3223  cbvral3v  3332  rspc6v  3585  ralxpxfr2d  3588  poeq1  5542  soeq1  5560  isoeq1  7272  isoeq2  7273  isoeq3  7274  fnmpoovd  8037  xpord3inddlem  8104  smoeq  8290  xpf1o  9077  nqereu  10852  dedekind  11309  dedekindle  11310  seqcaopr2  14000  wrd2ind  14685  addcn2  15556  mulcn2  15558  mreexexd  17614  catlid  17649  catrid  17650  isfunc  17831  funcres2b  17864  isfull  17879  isfth  17883  fullres2c  17908  isnat  17917  evlfcl  18188  uncfcurf  18205  isprs  18262  isdrs  18267  ispos  18280  istos  18382  resspos  18395  resstos  18396  isdlat  18488  ismgmhm  18664  issubmgm  18670  sgrp1  18697  ismhm  18753  issubm  18771  sgrp2nmndlem4  18899  isnsg  19130  isghm  19190  isghmOLD  19191  isga  19266  pmtrdifwrdel  19460  sylow2blem2  19596  efglem  19691  efgi  19694  efgredlemb  19721  efgred  19723  frgpuplem  19747  iscmn  19764  isomnd  20098  ring1  20291  isirred  20399  rnghmval  20420  isrnghm  20421  isorng  20838  islmod  20859  lmodlema  20860  lssset  20928  islssd  20930  islmhm  21022  islmhm2  21033  isobs  21700  dmatel  22458  dmatmulcl  22465  scmateALT  22477  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  cpmatel  22676  chpscmat  22807  hausnei2  23318  dfconn2  23384  llyeq  23435  nllyeq  23436  isucn2  24243  iducn  24247  ispsmet  24269  ismet  24288  isxmet  24289  metucn  24536  ngptgp  24601  nlmvscnlem1  24651  xmetdcn2  24803  addcnlem  24830  elcncf  24856  ipcnlem1  25212  cfili  25235  c1lip1  25964  aalioulem5  26302  aalioulem6  26303  aaliou  26304  aaliou2  26306  aaliou2b  26307  ulmcau  26360  ulmdvlem3  26367  cxpcn3lem  26711  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chpdifbndlem2  27517  pntrsumbnd2  27530  addsprop  27968  negsprop  28027  istrkgb  28523  axtgsegcon  28532  axtg5seg  28533  axtgpasch  28535  axtgeucl  28540  iscgrg  28580  isismt  28602  isperp2  28783  f1otrg  28939  axcontlem10  29042  axcontlem12  29044  iscusgredg  29492  isgrpo  30568  isablo  30617  vacn  30765  smcnlem  30768  lnoval  30823  islno  30824  isphg  30888  ajmoi  30929  ajval  30932  adjmo  31903  elcnop  31928  ellnop  31929  elunop  31943  elhmop  31944  elcnfn  31953  ellnfn  31954  adjeu  31960  adjval  31961  adj1  32004  adjeq  32006  cnlnadjlem9  32146  cnlnadjeu  32149  cnlnssadj  32151  isst  32284  ishst  32285  cdj1i  32504  cdj3i  32512  ismnt  33043  mgcval  33047  isslmd  33263  slmdlema  33264  prmidlval  33497  isprmidl  33498  isrprm  33577  qqhucn  34136  ismntop  34170  axtgupdim2ALTV  34812  txpconn  35414  nn0prpw  36505  heicant  37976  equivbnd  38111  isismty  38122  heibor1lem  38130  iccbnd  38161  isass  38167  elghomlem1OLD  38206  elghomlem2OLD  38207  isrngohom  38286  iscom2  38316  pridlval  38354  ispridl  38355  isdmn3  38395  inecmo  38676  islfl  39506  isopos  39626  psubspset  40190  islaut  40529  ispautN  40545  ltrnset  40564  isltrn  40565  istrnN  40603  istendo  41206  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones8  42592  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones15  42600  sn-isghm  43106  clsk1independent  44473  relpeq1  45371  relpeq2  45372  relpeq3  45373  sprsymrelfolem2  47953  sprsymrelfo  47957  reuopreuprim  47986  dmatALTbasel  48878  lindslinindsimp2  48939  lmod1  48968  isnrm4  49406  iscnrm4  49429  isuplem  49654  isthinc  49894  thincciso  49928  thinccisod  49929