Theorem 2ralbidv 3115

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (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 3112	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 3112	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 3038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3043

This theorem is referenced by:  cbvral3v  3308  ralxpxfr2d  3454  poeq1  5178  soeq1  5194  isoeq1  6718  isoeq2  6719  isoeq3  6720  fnmpt2ovd  7408  smoeq  7604  xpf1o  8275  nqereu  9914  dedekind  10363  dedekindle  10364  seqcaopr2  13002  wrd2ind  13648  addcn2  14494  mulcn2  14496  mreexexd  16481  catlid  16516  catrid  16517  isfunc  16696  funcres2b  16729  isfull  16742  isfth  16746  fullres2c  16771  isnat  16779  evlfcl  17034  uncfcurf  17051  isprs  17102  isdrs  17106  ispos  17119  istos  17207  isdlat  17365  sgrp1  17465  ismhm  17509  issubm  17519  sgrp2nmndlem4  17587  isnsg  17795  isghm  17832  isga  17895  pmtrdifwrdel  18076  sylow2blem2  18207  efglem  18300  efgi  18303  efgredlemb  18330  efgred  18332  frgpuplem  18356  iscmn  18371  ring1  18773  isirred  18870  islmod  19040  lmodlema  19041  lssset  19107  islssd  19109  islmhm  19200  islmhm2  19211  isobs  20237  dmatel  20472  dmatmulcl  20479  scmateALT  20491  mdetunilem3  20593  mdetunilem4  20594  mdetunilem9  20599  cpmatel  20689  chpscmat  20820  hausnei2  21330  dfconn2  21395  llyeq  21446  nllyeq  21447  isucn2  22255  iducn  22259  ispsmet  22281  ismet  22300  isxmet  22301  metucn  22548  ngptgp  22612  nlmvscnlem1  22662  xmetdcn2  22812  addcnlem  22839  elcncf  22864  ipcnlem1  23215  cfili  23237  c1lip1  23930  aalioulem5  24261  aalioulem6  24262  aaliou  24263  aaliou2  24265  aaliou2b  24266  ulmcau  24319  ulmdvlem3  24326  cxpcn3lem  24658  dvdsmulf1o  25090  chpdifbndlem2  25413  pntrsumbnd2  25426  istrkgb  25524  axtgsegcon  25533  axtg5seg  25534  axtgpasch  25536  axtgeucl  25541  iscgrg  25577  isismt  25599  isperp2  25780  f1otrg  25921  axcontlem10  26023  axcontlem12  26025  isgrpo  27631  isablo  27680  vacn  27829  smcnlem  27832  lnoval  27887  islno  27888  isphg  27952  ajmoi  27994  ajval  27997  adjmo  28971  elcnop  28996  ellnop  28997  elunop  29011  elhmop  29012  elcnfn  29021  ellnfn  29022  adjeu  29028  adjval  29029  adj1  29072  adjeq  29074  cnlnadjlem9  29214  cnlnadjeu  29217  cnlnssadj  29219  isst  29352  ishst  29353  cdj1i  29572  cdj3i  29580  resspos  29939  resstos  29940  isomnd  29981  isslmd  30035  slmdlema  30036  isorng  30079  qqhucn  30316  ismntop  30350  axtgupdim2OLD  31026  txpconn  31492  nn0prpw  32595  heicant  33726  equivbnd  33871  isismty  33882  heibor1lem  33890  iccbnd  33921  isass  33927  elghomlem1OLD  33966  elghomlem2OLD  33967  isrngohom  34046  iscom2  34076  pridlval  34114  ispridl  34115  isdmn3  34155  inecmo  34412  islfl  34819  isopos  34939  psubspset  35502  islaut  35841  ispautN  35857  ltrnset  35876  isltrn  35877  istrnN  35916  istendo  36519  clsk1independent  38815  sprsymrelfolem2  42222  sprsymrelfo  42226  ismgmhm  42262  issubmgm  42268  isrnghm  42371  lidlmsgrp  42405  lidlrng  42406  dmatALTbasel  42670  lindslinindsimp2  42731  lmod1  42760