Theorem 2ralbidv 3221

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3061

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062

This theorem is referenced by:  3ralbidv  3224  6ralbidv  3226  cbvral3vw  3243  cbvral6vw  3245  cbvral3v  3370  rspc6v  3643  ralxpxfr2d  3646  poeq1  5595  soeq1  5613  isoeq1  7337  isoeq2  7338  isoeq3  7339  fnmpoovd  8112  xpord3inddlem  8179  smoeq  8390  xpf1o  9179  nqereu  10969  dedekind  11424  dedekindle  11425  seqcaopr2  14079  wrd2ind  14761  addcn2  15630  mulcn2  15632  mreexexd  17691  catlid  17726  catrid  17727  isfunc  17909  funcres2b  17942  isfull  17957  isfth  17961  fullres2c  17986  isnat  17995  evlfcl  18267  uncfcurf  18284  isprs  18342  isdrs  18347  ispos  18360  istos  18463  isdlat  18567  ismgmhm  18709  issubmgm  18715  sgrp1  18742  ismhm  18798  issubm  18816  sgrp2nmndlem4  18941  isnsg  19173  isghm  19233  isghmOLD  19234  isga  19309  pmtrdifwrdel  19503  sylow2blem2  19639  efglem  19734  efgi  19737  efgredlemb  19764  efgred  19766  frgpuplem  19790  iscmn  19807  ring1  20307  isirred  20419  rnghmval  20440  isrnghm  20441  islmod  20862  lmodlema  20863  lssset  20931  islssd  20933  islmhm  21026  islmhm2  21037  isobs  21740  dmatel  22499  dmatmulcl  22506  scmateALT  22518  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  cpmatel  22717  chpscmat  22848  hausnei2  23361  dfconn2  23427  llyeq  23478  nllyeq  23479  isucn2  24288  iducn  24292  ispsmet  24314  ismet  24333  isxmet  24334  metucn  24584  ngptgp  24649  nlmvscnlem1  24707  xmetdcn2  24859  addcnlem  24886  elcncf  24915  ipcnlem1  25279  cfili  25302  c1lip1  26036  aalioulem5  26378  aalioulem6  26379  aaliou  26380  aaliou2  26382  aaliou2b  26383  ulmcau  26438  ulmdvlem3  26445  cxpcn3lem  26790  mpodvdsmulf1o  27237  dvdsmulf1o  27239  chpdifbndlem2  27598  pntrsumbnd2  27611  addsprop  28009  negsprop  28067  istrkgb  28463  axtgsegcon  28472  axtg5seg  28473  axtgpasch  28475  axtgeucl  28480  iscgrg  28520  isismt  28542  isperp2  28723  f1otrg  28879  axcontlem10  28988  axcontlem12  28990  iscusgredg  29440  isgrpo  30516  isablo  30565  vacn  30713  smcnlem  30716  lnoval  30771  islno  30772  isphg  30836  ajmoi  30877  ajval  30880  adjmo  31851  elcnop  31876  ellnop  31877  elunop  31891  elhmop  31892  elcnfn  31901  ellnfn  31902  adjeu  31908  adjval  31909  adj1  31952  adjeq  31954  cnlnadjlem9  32094  cnlnadjeu  32097  cnlnssadj  32099  isst  32232  ishst  32233  cdj1i  32452  cdj3i  32460  resspos  32956  resstos  32957  ismnt  32973  mgcval  32977  isomnd  33078  isslmd  33208  slmdlema  33209  isorng  33329  prmidlval  33465  isprmidl  33466  isrprm  33545  qqhucn  33993  ismntop  34027  axtgupdim2ALTV  34683  txpconn  35237  nn0prpw  36324  heicant  37662  equivbnd  37797  isismty  37808  heibor1lem  37816  iccbnd  37847  isass  37853  elghomlem1OLD  37892  elghomlem2OLD  37893  isrngohom  37972  iscom2  38002  pridlval  38040  ispridl  38041  isdmn3  38081  inecmo  38356  islfl  39061  isopos  39181  psubspset  39746  islaut  40085  ispautN  40101  ltrnset  40120  isltrn  40121  istrnN  40159  istendo  40762  sticksstones1  42147  sticksstones2  42148  sticksstones3  42149  sticksstones8  42154  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones15  42162  sn-isghm  42683  clsk1independent  44059  relpeq1  44965  relpeq2  44966  relpeq3  44967  sprsymrelfolem2  47480  sprsymrelfo  47484  reuopreuprim  47513  dmatALTbasel  48319  lindslinindsimp2  48380  lmod1  48409  isnrm4  48828  iscnrm4  48851  isuplem  48936  isthinc  49069  thincciso  49102  thinccisod  49103