Theorem 2ralbidv 3216

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3059

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  3ralbidv  3219  6ralbidv  3221  cbvral3vw  3238  cbvral6vw  3240  cbvral3v  3364  rspc6v  3630  ralxpxfr2d  3633  poeq1  5590  soeq1  5608  isoeq1  7316  isoeq2  7317  isoeq3  7318  fnmpoovd  8075  xpord3inddlem  8142  smoeq  8352  xpf1o  9141  nqereu  10926  dedekind  11381  dedekindle  11382  seqcaopr2  14008  wrd2ind  14677  addcn2  15542  mulcn2  15544  mreexexd  17596  catlid  17631  catrid  17632  isfunc  17818  funcres2b  17851  isfull  17865  isfth  17869  fullres2c  17894  isnat  17902  evlfcl  18179  uncfcurf  18196  isprs  18254  isdrs  18258  ispos  18271  istos  18375  isdlat  18479  ismgmhm  18621  issubmgm  18627  sgrp1  18654  ismhm  18707  issubm  18720  sgrp2nmndlem4  18845  isnsg  19071  isghm  19130  isga  19196  pmtrdifwrdel  19394  sylow2blem2  19530  efglem  19625  efgi  19628  efgredlemb  19655  efgred  19657  frgpuplem  19681  iscmn  19698  ring1  20198  isirred  20310  rnghmval  20331  isrnghm  20332  islmod  20618  lmodlema  20619  lssset  20688  islssd  20690  islmhm  20782  islmhm2  20793  isobs  21494  dmatel  22215  dmatmulcl  22222  scmateALT  22234  mdetunilem3  22336  mdetunilem4  22337  mdetunilem9  22342  cpmatel  22433  chpscmat  22564  hausnei2  23077  dfconn2  23143  llyeq  23194  nllyeq  23195  isucn2  24004  iducn  24008  ispsmet  24030  ismet  24049  isxmet  24050  metucn  24300  ngptgp  24365  nlmvscnlem1  24423  xmetdcn2  24573  addcnlem  24600  elcncf  24629  ipcnlem1  24993  cfili  25016  c1lip1  25749  aalioulem5  26085  aalioulem6  26086  aaliou  26087  aaliou2  26089  aaliou2b  26090  ulmcau  26143  ulmdvlem3  26150  cxpcn3lem  26491  dvdsmulf1o  26934  chpdifbndlem2  27293  pntrsumbnd2  27306  addsprop  27698  negsprop  27748  istrkgb  27973  axtgsegcon  27982  axtg5seg  27983  axtgpasch  27985  axtgeucl  27990  iscgrg  28030  isismt  28052  isperp2  28233  f1otrg  28389  axcontlem10  28498  axcontlem12  28500  iscusgredg  28947  isgrpo  30017  isablo  30066  vacn  30214  smcnlem  30217  lnoval  30272  islno  30273  isphg  30337  ajmoi  30378  ajval  30381  adjmo  31352  elcnop  31377  ellnop  31378  elunop  31392  elhmop  31393  elcnfn  31402  ellnfn  31403  adjeu  31409  adjval  31410  adj1  31453  adjeq  31455  cnlnadjlem9  31595  cnlnadjeu  31598  cnlnssadj  31600  isst  31733  ishst  31734  cdj1i  31953  cdj3i  31961  resspos  32403  resstos  32404  ismnt  32420  mgcval  32424  isomnd  32489  isslmd  32617  slmdlema  32618  isorng  32687  prmidlval  32829  isprmidl  32830  isrprm  32908  qqhucn  33270  ismntop  33304  axtgupdim2ALTV  33978  txpconn  34521  nn0prpw  35511  heicant  36826  equivbnd  36961  isismty  36972  heibor1lem  36980  iccbnd  37011  isass  37017  elghomlem1OLD  37056  elghomlem2OLD  37057  isrngohom  37136  iscom2  37166  pridlval  37204  ispridl  37205  isdmn3  37245  inecmo  37527  islfl  38233  isopos  38353  psubspset  38918  islaut  39257  ispautN  39273  ltrnset  39292  isltrn  39293  istrnN  39331  istendo  39934  sticksstones1  41268  sticksstones2  41269  sticksstones3  41270  sticksstones8  41275  sticksstones10  41277  sticksstones11  41278  sticksstones12a  41279  sticksstones15  41283  clsk1independent  43099  sprsymrelfolem2  46459  sprsymrelfo  46463  reuopreuprim  46492  dmatALTbasel  47170  lindslinindsimp2  47231  lmod1  47260  isnrm4  47650  iscnrm4  47674  isthinc  47728  thincciso  47756