Theorem 2ralbidv 3226

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

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

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 3077

This theorem is used by:  3ralbidv  3229  6ralbidv  3231  cbvral3vw  3246  cbvral6vw  3248  cbvral3v  3355  rspc6v  3597  ralxpxfr2d  3600  poeq1  5566  soeq1  5584  isoeq1  7319  isoeq2  7320  isoeq3  7321  fnmpoovd  8085  xpord3inddlem  8153  smoeq  8340  xpf1o  9140  nqereu  10941  dedekind  11400  dedekindle  11401  seqcaopr2  14105  wrd2ind  14795  addcn2  15684  mulcn2  15686  mreexexd  17739  catlid  17774  catrid  17775  isfunc  17956  funcres2b  17989  isfull  18004  isfth  18008  fullres2c  18033  isnat  18042  evlfcl  18313  uncfcurf  18330  isprs  18387  isdrs  18392  ispos  18405  istos  18507  resspos  18520  resstos  18521  isdlat  18613  ismgmhm  18801  issubmgm  18807  sgrp1  18834  ismhm  18896  issubm  18914  sgrp2nmndlem4  19043  isnsg  19281  isghm  19346  isga  19421  pmtrdifwrdel  19615  sylow2blem2  19751  efglem  19846  efgi  19849  efgredlemb  19876  efgred  19878  frgpuplem  19902  iscmn  19919  isomnd  20253  ring1  20455  isirred  20563  rnghmval  20584  isrnghm  20585  rhmval0  20619  isrhm0  20620  isorng  21030  islmod  21051  lmodlema  21052  lssset  21120  islssd  21122  islmhm  21214  islmhm2  21225  prmidlval  21528  isprmidl  21529  isobs  21936  dmatel  22718  dmatmulcl  22725  scmateALT  22737  mdetunilem3  22839  mdetunilem4  22840  mdetunilem9  22845  cpmatel  22939  chpscmat  23070  hausnei2  23581  dfconn2  23647  llyeq  23699  nllyeq  23700  isucn2  24507  iducn  24511  ispsmet  24533  ismet  24552  isxmet  24553  metucn  24800  ngptgp  24865  nlmvscnlem1  24915  xmetdcn2  25067  addcnlem  25094  elcncf  25120  ipcnlem1  25476  cfili  25499  c1lip1  26227  aalioulem5  26575  aalioulem6  26576  aaliou  26577  aaliou2  26579  aaliou2b  26580  ulmcau  26634  ulmdvlem3  26641  cxpcn3lem  26987  mpodvdsmulf1o  27433  dvdsmulf1o  27435  chpdifbndlem2  27793  pntrsumbnd2  27806  addsprop  28244  negsprop  28303  istrkgb  28799  axtgsegcon  28808  axtg5seg  28809  axtgpasch  28811  axtgeucl  28816  iscgrg  28857  isismt  28879  isperp2  29072  f1otrg  29330  axcontlem10  29433  axcontlem12  29435  iscusgredg  29886  isgrpo  30981  isablo  31030  vacn  31178  smcnlem  31181  lnoval  31236  islno  31237  isphg  31301  ajmoi  31342  ajval  31345  adjmo  32316  elcnop  32341  ellnop  32342  elunop  32356  elhmop  32357  elcnfn  32366  ellnfn  32367  adjeu  32373  adjval  32374  adj1  32417  adjeq  32419  cnlnadjlem9  32559  cnlnadjeu  32562  cnlnssadj  32564  isst  32697  ishst  32698  cdj1i  32917  cdj3i  32925  ismnt  33426  mgcval  33430  isslmd  33645  slmdlema  33646  isrprm  33930  qqhucn  34505  ismntop  34539  axtgupdim2ALTV  35179  txpconn  35814  nmulprop  36773  nmulr0  36778  nmuladdel  36795  ltnmul  36799  nn0prpw  36945  heicant  38407  equivbnd  38543  isismty  38554  heibor1lem  38562  iccbnd  38593  isass  38599  elghomlem1OLD  38638  elghomlem2OLD  38639  isrngohom  38718  iscom2  38748  pridlval  38786  ispridl  38787  isdmn3  38827  inecmo  39106  islfl  39936  isopos  40056  psubspset  40620  islaut  40959  ispautN  40975  ltrnset  40994  isltrn  40995  istrnN  41033  istendo  41636  sticksstones1  43015  sticksstones2  43016  sticksstones3  43017  sticksstones8  43022  sticksstones10  43024  sticksstones11  43025  sticksstones12a  43026  sticksstones15  43030  sn-isghm  43522  clsk1independent  44889  relpeq1  45770  relpeq2  45771  relpeq3  45772  sprsymrelfolem2  48396  sprsymrelfo  48400  reuopreuprim  48429  isidom3  49263  dmatALTbasel  49335  lindslinindsimp2  49396  lmod1  49425  isnrm4  49860  iscnrm4  49883  isuplem  50108  isthinc  50348  thincciso  50382  thinccisod  50383