Theorem 2ralbidv 3203

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3054

This theorem is referenced by:  3ralbidv  3206  6ralbidv  3208  cbvral3vw  3223  cbvral6vw  3225  cbvral3v  3334  rspc6v  3581  ralxpxfr2d  3584  poeq1  5530  soeq1  5548  isoeq1  7262  isoeq2  7263  isoeq3  7264  fnmpoovd  8027  xpord3inddlem  8095  smoeq  8281  xpf1o  9068  nqereu  10844  dedekind  11301  dedekindle  11302  seqcaopr2  13992  wrd2ind  14677  addcn2  15548  mulcn2  15550  mreexexd  17606  catlid  17641  catrid  17642  isfunc  17823  funcres2b  17856  isfull  17871  isfth  17875  fullres2c  17900  isnat  17909  evlfcl  18180  uncfcurf  18197  isprs  18254  isdrs  18259  ispos  18272  istos  18374  resspos  18387  resstos  18388  isdlat  18480  ismgmhm  18656  issubmgm  18662  sgrp1  18689  ismhm  18745  issubm  18763  sgrp2nmndlem4  18891  isnsg  19122  isghm  19182  isghmOLD  19183  isga  19258  pmtrdifwrdel  19452  sylow2blem2  19588  efglem  19683  efgi  19686  efgredlemb  19713  efgred  19715  frgpuplem  19739  iscmn  19756  isomnd  20090  ring1  20283  isirred  20391  rnghmval  20412  isrnghm  20413  isorng  20834  islmod  20855  lmodlema  20856  lssset  20924  islssd  20926  islmhm  21018  islmhm2  21029  isobs  21696  dmatel  22477  dmatmulcl  22484  scmateALT  22496  mdetunilem3  22598  mdetunilem4  22599  mdetunilem9  22604  cpmatel  22695  chpscmat  22826  hausnei2  23337  dfconn2  23403  llyeq  23454  nllyeq  23455  isucn2  24262  iducn  24266  ispsmet  24288  ismet  24307  isxmet  24308  metucn  24555  ngptgp  24620  nlmvscnlem1  24670  xmetdcn2  24822  addcnlem  24849  elcncf  24875  ipcnlem1  25231  cfili  25254  c1lip1  25983  aalioulem5  26321  aalioulem6  26322  aaliou  26323  aaliou2  26325  aaliou2b  26326  ulmcau  26379  ulmdvlem3  26386  cxpcn3lem  26730  mpodvdsmulf1o  27176  dvdsmulf1o  27178  chpdifbndlem2  27536  pntrsumbnd2  27549  addsprop  27987  negsprop  28046  istrkgb  28542  axtgsegcon  28551  axtg5seg  28552  axtgpasch  28554  axtgeucl  28559  iscgrg  28599  isismt  28621  isperp2  28802  f1otrg  28958  axcontlem10  29061  axcontlem12  29063  iscusgredg  29511  isgrpo  30587  isablo  30636  vacn  30784  smcnlem  30787  lnoval  30842  islno  30843  isphg  30907  ajmoi  30948  ajval  30951  adjmo  31922  elcnop  31947  ellnop  31948  elunop  31962  elhmop  31963  elcnfn  31972  ellnfn  31973  adjeu  31979  adjval  31980  adj1  32023  adjeq  32025  cnlnadjlem9  32165  cnlnadjeu  32168  cnlnssadj  32170  isst  32303  ishst  32304  cdj1i  32523  cdj3i  32531  ismnt  33063  mgcval  33067  isslmd  33284  slmdlema  33285  prmidlval  33521  isprmidl  33522  isrprm  33609  qqhucn  34185  ismntop  34219  axtgupdim2ALTV  34861  txpconn  35469  nn0prpw  36560  heicant  38031  equivbnd  38166  isismty  38177  heibor1lem  38185  iccbnd  38216  isass  38222  elghomlem1OLD  38261  elghomlem2OLD  38262  isrngohom  38341  iscom2  38371  pridlval  38409  ispridl  38410  isdmn3  38450  inecmo  38731  islfl  39561  isopos  39681  psubspset  40245  islaut  40584  ispautN  40600  ltrnset  40619  isltrn  40620  istrnN  40658  istendo  41261  sticksstones1  42640  sticksstones2  42641  sticksstones3  42642  sticksstones8  42647  sticksstones10  42649  sticksstones11  42650  sticksstones12a  42651  sticksstones15  42655  sn-isghm  43132  clsk1independent  44499  relpeq1  45397  relpeq2  45398  relpeq3  45399  sprsymrelfolem2  47976  sprsymrelfo  47980  reuopreuprim  48009  dmatALTbasel  48901  lindslinindsimp2  48962  lmod1  48991  isnrm4  49429  iscnrm4  49452  isuplem  49677  isthinc  49917  thincciso  49951  thinccisod  49952