Theorem 2ralbidv 3227

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

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

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 3078

This theorem is used by:  3ralbidv  3230  6ralbidv  3232  cbvral3vw  3247  cbvral6vw  3249  cbvral3v  3356  rspc6v  3597  ralxpxfr2d  3600  poeq1  5562  soeq1  5580  isoeq1  7325  isoeq2  7326  isoeq3  7327  fnmpoovd  8098  xpord3inddlem  8171  smoeq  8358  xpf1o  9158  nqereu  11014  dedekind  11473  dedekindle  11474  seqcaopr2  14181  wrd2ind  14872  addcn2  15761  mulcn2  15763  mreexexd  17822  catlid  17857  catrid  17858  isfunc  18039  funcres2b  18072  isfull  18087  isfth  18091  fullres2c  18116  isnat  18125  evlfcl  18396  uncfcurf  18413  isprs  18470  isdrs  18475  ispos  18488  istos  18590  resspos  18603  resstos  18604  isdlat  18696  ismgmhm  18885  issubmgm  18891  sgrp1  18918  ismhm  18980  issubm  18998  sgrp2nmndlem4  19127  isnsg  19365  isghm  19430  isga  19505  pmtrdifwrdel  19699  sylow2blem2  19835  efglem  19930  efgi  19933  efgredlemb  19960  efgred  19962  frgpuplem  19986  iscmn  20003  isomnd  20337  ring1  20541  isirred  20649  rnghmval  20670  isrnghm  20671  rhmval0  20705  isrhm0  20706  isorng  21118  islmod  21139  lmodlema  21140  lssset  21208  islssd  21210  islmhm  21302  islmhm2  21313  prmidlval  21618  isprmidl  21619  isobs  22026  dmatel  22808  dmatmulcl  22815  scmateALT  22827  mdetunilem3  22929  mdetunilem4  22930  mdetunilem9  22935  cpmatel  23029  chpscmat  23160  hausnei2  23671  dfconn2  23737  llyeq  23789  nllyeq  23790  isucn2  24597  iducn  24601  ispsmet  24623  ismet  24642  isxmet  24643  metucn  24890  ngptgp  24955  nlmvscnlem1  25005  xmetdcn2  25157  addcnlem  25184  elcncf  25210  ipcnlem1  25566  cfili  25589  c1lip1  26317  aalioulem5  26663  aalioulem6  26664  aaliou  26665  aaliou2  26667  aaliou2b  26668  ulmcau  26722  ulmdvlem3  26729  cxpcn3lem  27075  mpodvdsmulf1o  27521  dvdsmulf1o  27523  chpdifbndlem2  27881  pntrsumbnd2  27894  addsprop  28362  negsprop  28421  istrkgb  28917  axtgsegcon  28926  axtg5seg  28927  axtgpasch  28929  axtgeucl  28934  iscgrg  28975  isismt  28997  isperp2  29190  f1otrg  29448  axcontlem10  29551  axcontlem12  29553  iscusgredg  30004  isgrpo  31099  isablo  31148  vacn  31296  smcnlem  31299  lnoval  31354  islno  31355  isphg  31419  ajmoi  31460  ajval  31463  adjmo  32434  elcnop  32459  ellnop  32460  elunop  32474  elhmop  32475  elcnfn  32484  ellnfn  32485  adjeu  32491  adjval  32492  adj1  32535  adjeq  32537  cnlnadjlem9  32677  cnlnadjeu  32680  cnlnssadj  32682  isst  32815  ishst  32816  cdj1i  33035  cdj3i  33043  ismnt  33544  mgcval  33548  isslmd  33763  slmdlema  33764  isrprm  34049  qqhucn  34624  ismntop  34658  axtgupdim2ALTV  35297  txpconn  35997  nmulprop  36939  nmulr0  36944  nmuladdel  36961  ltnmul  36965  nn0prpw  37111  heicant  38573  equivbnd  38724  isismty  38735  heibor1lem  38743  iccbnd  38774  isass  38780  elghomlem1OLD  38819  elghomlem2OLD  38820  isrngohom  38899  iscom2  38929  pridlval  38967  ispridl  38968  isdmn3  39008  inecmo  39287  islfl  40117  isopos  40237  psubspset  40801  islaut  41140  ispautN  41156  ltrnset  41175  isltrn  41176  istrnN  41214  istendo  41817  sticksstones1  43196  sticksstones2  43197  sticksstones3  43198  sticksstones8  43203  sticksstones10  43205  sticksstones11  43206  sticksstones12a  43207  sticksstones15  43211  sn-isghm  43684  clsk1independent  45045  relpeq1  45933  relpeq2  45934  relpeq3  45935  sprsymrelfolem2  48574  sprsymrelfo  48578  reuopreuprim  48607  isidom3  49441  dmatALTbasel  49513  lindslinindsimp2  49574  lmod1  49603  isnrm4  50038  iscnrm4  50061  isuplem  50286  isthinc  50526  thincciso  50560  thinccisod  50561