Theorem 2ralbidv 3219

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 205  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  3ralbidv  3222  6ralbidv  3224  cbvral3vw  3241  cbvral6vw  3243  cbvral3v  3367  rspc6v  3632  ralxpxfr2d  3635  poeq1  5592  soeq1  5610  isoeq1  7314  isoeq2  7315  isoeq3  7316  fnmpoovd  8073  xpord3inddlem  8140  smoeq  8350  xpf1o  9139  nqereu  10924  dedekind  11377  dedekindle  11378  seqcaopr2  14004  wrd2ind  14673  addcn2  15538  mulcn2  15540  mreexexd  17592  catlid  17627  catrid  17628  isfunc  17814  funcres2b  17847  isfull  17861  isfth  17865  fullres2c  17890  isnat  17898  evlfcl  18175  uncfcurf  18192  isprs  18250  isdrs  18254  ispos  18267  istos  18371  isdlat  18475  sgrp1  18620  ismhm  18673  issubm  18684  sgrp2nmndlem4  18809  isnsg  19035  isghm  19092  isga  19155  pmtrdifwrdel  19353  sylow2blem2  19489  efglem  19584  efgi  19587  efgredlemb  19614  efgred  19616  frgpuplem  19640  iscmn  19657  ring1  20122  isirred  20233  islmod  20475  lmodlema  20476  lssset  20544  islssd  20546  islmhm  20638  islmhm2  20649  isobs  21275  dmatel  21995  dmatmulcl  22002  scmateALT  22014  mdetunilem3  22116  mdetunilem4  22117  mdetunilem9  22122  cpmatel  22213  chpscmat  22344  hausnei2  22857  dfconn2  22923  llyeq  22974  nllyeq  22975  isucn2  23784  iducn  23788  ispsmet  23810  ismet  23829  isxmet  23830  metucn  24080  ngptgp  24145  nlmvscnlem1  24203  xmetdcn2  24353  addcnlem  24380  elcncf  24405  ipcnlem1  24762  cfili  24785  c1lip1  25514  aalioulem5  25849  aalioulem6  25850  aaliou  25851  aaliou2  25853  aaliou2b  25854  ulmcau  25907  ulmdvlem3  25914  cxpcn3lem  26255  dvdsmulf1o  26698  chpdifbndlem2  27057  pntrsumbnd2  27070  addsprop  27460  negsprop  27509  istrkgb  27706  axtgsegcon  27715  axtg5seg  27716  axtgpasch  27718  axtgeucl  27723  iscgrg  27763  isismt  27785  isperp2  27966  f1otrg  28122  axcontlem10  28231  axcontlem12  28233  iscusgredg  28680  isgrpo  29750  isablo  29799  vacn  29947  smcnlem  29950  lnoval  30005  islno  30006  isphg  30070  ajmoi  30111  ajval  30114  adjmo  31085  elcnop  31110  ellnop  31111  elunop  31125  elhmop  31126  elcnfn  31135  ellnfn  31136  adjeu  31142  adjval  31143  adj1  31186  adjeq  31188  cnlnadjlem9  31328  cnlnadjeu  31331  cnlnssadj  31333  isst  31466  ishst  31467  cdj1i  31686  cdj3i  31694  resspos  32136  resstos  32137  ismnt  32153  mgcval  32157  isomnd  32219  isslmd  32347  slmdlema  32348  isorng  32417  prmidlval  32555  isprmidl  32556  isrprm  32634  qqhucn  32972  ismntop  33006  axtgupdim2ALTV  33680  txpconn  34223  nn0prpw  35208  heicant  36523  equivbnd  36658  isismty  36669  heibor1lem  36677  iccbnd  36708  isass  36714  elghomlem1OLD  36753  elghomlem2OLD  36754  isrngohom  36833  iscom2  36863  pridlval  36901  ispridl  36902  isdmn3  36942  inecmo  37224  islfl  37930  isopos  38050  psubspset  38615  islaut  38954  ispautN  38970  ltrnset  38989  isltrn  38990  istrnN  39028  istendo  39631  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones8  40969  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones15  40977  clsk1independent  42797  sprsymrelfolem2  46161  sprsymrelfo  46165  reuopreuprim  46194  ismgmhm  46553  issubmgm  46559  rnghmval  46689  isrnghm  46690  dmatALTbasel  47083  lindslinindsimp2  47144  lmod1  47173  isnrm4  47563  iscnrm4  47587  isthinc  47641  thincciso  47669