Theorem 2ralbidv 3194

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  3ralbidv  3197  6ralbidv  3199  cbvral3vw  3214  cbvral6vw  3216  cbvral3v  3334  rspc6v  3596  ralxpxfr2d  3599  poeq1  5525  soeq1  5543  isoeq1  7246  isoeq2  7247  isoeq3  7248  fnmpoovd  8012  xpord3inddlem  8079  smoeq  8265  xpf1o  9047  nqereu  10812  dedekind  11268  dedekindle  11269  seqcaopr2  13937  wrd2ind  14622  addcn2  15493  mulcn2  15495  mreexexd  17546  catlid  17581  catrid  17582  isfunc  17763  funcres2b  17796  isfull  17811  isfth  17815  fullres2c  17840  isnat  17849  evlfcl  18120  uncfcurf  18137  isprs  18194  isdrs  18199  ispos  18212  istos  18314  resspos  18327  resstos  18328  isdlat  18420  ismgmhm  18596  issubmgm  18602  sgrp1  18629  ismhm  18685  issubm  18703  sgrp2nmndlem4  18828  isnsg  19060  isghm  19120  isghmOLD  19121  isga  19196  pmtrdifwrdel  19390  sylow2blem2  19526  efglem  19621  efgi  19624  efgredlemb  19651  efgred  19653  frgpuplem  19677  iscmn  19694  isomnd  20028  ring1  20221  isirred  20330  rnghmval  20351  isrnghm  20352  isorng  20769  islmod  20790  lmodlema  20791  lssset  20859  islssd  20861  islmhm  20954  islmhm2  20965  isobs  21650  dmatel  22401  dmatmulcl  22408  scmateALT  22420  mdetunilem3  22522  mdetunilem4  22523  mdetunilem9  22528  cpmatel  22619  chpscmat  22750  hausnei2  23261  dfconn2  23327  llyeq  23378  nllyeq  23379  isucn2  24186  iducn  24190  ispsmet  24212  ismet  24231  isxmet  24232  metucn  24479  ngptgp  24544  nlmvscnlem1  24594  xmetdcn2  24746  addcnlem  24773  elcncf  24802  ipcnlem1  25165  cfili  25188  c1lip1  25922  aalioulem5  26264  aalioulem6  26265  aaliou  26266  aaliou2  26268  aaliou2b  26269  ulmcau  26324  ulmdvlem3  26331  cxpcn3lem  26677  mpodvdsmulf1o  27124  dvdsmulf1o  27126  chpdifbndlem2  27485  pntrsumbnd2  27498  addsprop  27912  negsprop  27970  istrkgb  28426  axtgsegcon  28435  axtg5seg  28436  axtgpasch  28438  axtgeucl  28443  iscgrg  28483  isismt  28505  isperp2  28686  f1otrg  28842  axcontlem10  28944  axcontlem12  28946  iscusgredg  29394  isgrpo  30467  isablo  30516  vacn  30664  smcnlem  30667  lnoval  30722  islno  30723  isphg  30787  ajmoi  30828  ajval  30831  adjmo  31802  elcnop  31827  ellnop  31828  elunop  31842  elhmop  31843  elcnfn  31852  ellnfn  31853  adjeu  31859  adjval  31860  adj1  31903  adjeq  31905  cnlnadjlem9  32045  cnlnadjeu  32048  cnlnssadj  32050  isst  32183  ishst  32184  cdj1i  32403  cdj3i  32411  ismnt  32954  mgcval  32958  isslmd  33161  slmdlema  33162  prmidlval  33392  isprmidl  33393  isrprm  33472  qqhucn  33995  ismntop  34029  axtgupdim2ALTV  34671  txpconn  35244  nn0prpw  36336  heicant  37674  equivbnd  37809  isismty  37820  heibor1lem  37828  iccbnd  37859  isass  37865  elghomlem1OLD  37904  elghomlem2OLD  37905  isrngohom  37984  iscom2  38014  pridlval  38052  ispridl  38053  isdmn3  38093  inecmo  38362  islfl  39078  isopos  39198  psubspset  39762  islaut  40101  ispautN  40117  ltrnset  40136  isltrn  40137  istrnN  40175  istendo  40778  sticksstones1  42158  sticksstones2  42159  sticksstones3  42160  sticksstones8  42165  sticksstones10  42167  sticksstones11  42168  sticksstones12a  42169  sticksstones15  42173  sn-isghm  42685  clsk1independent  44058  relpeq1  44956  relpeq2  44957  relpeq3  44958  sprsymrelfolem2  47503  sprsymrelfo  47507  reuopreuprim  47536  dmatALTbasel  48413  lindslinindsimp2  48474  lmod1  48503  isnrm4  48941  iscnrm4  48964  isuplem  49190  isthinc  49430  thincciso  49464  thinccisod  49465