Theorem 2ralbidv 3209

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 3171	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 3171	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 1796  ax-4 1810  ax-5 1912

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

This theorem is referenced by:  cbvral3vw  3226  cbvral3v  3340  ralxpxfr2d  3585  poeq1  5524  soeq1  5542  isoeq1  7227  isoeq2  7228  isoeq3  7229  fnmpoovd  7972  smoeq  8228  xpf1o  8981  nqereu  10758  dedekind  11211  dedekindle  11212  seqcaopr2  13832  wrd2ind  14508  addcn2  15375  mulcn2  15377  mreexexd  17427  catlid  17462  catrid  17463  isfunc  17649  funcres2b  17682  isfull  17696  isfth  17700  fullres2c  17725  isnat  17733  evlfcl  18010  uncfcurf  18027  isprs  18085  isdrs  18089  ispos  18102  istos  18206  isdlat  18310  sgrp1  18454  ismhm  18502  issubm  18512  sgrp2nmndlem4  18636  isnsg  18852  isghm  18903  isga  18966  pmtrdifwrdel  19162  sylow2blem2  19295  efglem  19390  efgi  19393  efgredlemb  19420  efgred  19422  frgpuplem  19446  iscmn  19462  ring1  19909  isirred  20009  islmod  20199  lmodlema  20200  lssset  20267  islssd  20269  islmhm  20361  islmhm2  20372  isobs  20999  dmatel  21714  dmatmulcl  21721  scmateALT  21733  mdetunilem3  21835  mdetunilem4  21836  mdetunilem9  21841  cpmatel  21932  chpscmat  22063  hausnei2  22576  dfconn2  22642  llyeq  22693  nllyeq  22694  isucn2  23503  iducn  23507  ispsmet  23529  ismet  23548  isxmet  23549  metucn  23799  ngptgp  23864  nlmvscnlem1  23922  xmetdcn2  24072  addcnlem  24099  elcncf  24124  ipcnlem1  24481  cfili  24504  c1lip1  25233  aalioulem5  25568  aalioulem6  25569  aaliou  25570  aaliou2  25572  aaliou2b  25573  ulmcau  25626  ulmdvlem3  25633  cxpcn3lem  25972  dvdsmulf1o  26415  chpdifbndlem2  26774  pntrsumbnd2  26787  istrkgb  26925  axtgsegcon  26934  axtg5seg  26935  axtgpasch  26937  axtgeucl  26942  iscgrg  26982  isismt  27004  isperp2  27185  f1otrg  27341  axcontlem10  27450  axcontlem12  27452  iscusgredg  27899  isgrpo  28968  isablo  29017  vacn  29165  smcnlem  29168  lnoval  29223  islno  29224  isphg  29288  ajmoi  29329  ajval  29332  adjmo  30303  elcnop  30328  ellnop  30329  elunop  30343  elhmop  30344  elcnfn  30353  ellnfn  30354  adjeu  30360  adjval  30361  adj1  30404  adjeq  30406  cnlnadjlem9  30546  cnlnadjeu  30549  cnlnssadj  30551  isst  30684  ishst  30685  cdj1i  30904  cdj3i  30912  resspos  31352  resstos  31353  ismnt  31369  mgcval  31373  isomnd  31435  isslmd  31563  slmdlema  31564  isorng  31606  prmidlval  31717  isprmidl  31718  isrprm  31770  qqhucn  32048  ismntop  32082  axtgupdim2ALTV  32754  txpconn  33299  xpord3ind  33898  nn0prpw  34570  heicant  35868  equivbnd  36004  isismty  36015  heibor1lem  36023  iccbnd  36054  isass  36060  elghomlem1OLD  36099  elghomlem2OLD  36100  isrngohom  36179  iscom2  36209  pridlval  36247  ispridl  36248  isdmn3  36288  inecmo  36572  islfl  37278  isopos  37398  psubspset  37963  islaut  38302  ispautN  38318  ltrnset  38337  isltrn  38338  istrnN  38376  istendo  38979  sticksstones1  40310  sticksstones2  40311  sticksstones3  40312  sticksstones8  40317  sticksstones10  40319  sticksstones11  40320  sticksstones12a  40321  sticksstones15  40325  clsk1independent  41877  sprsymrelfolem2  45197  sprsymrelfo  45201  reuopreuprim  45230  ismgmhm  45589  issubmgm  45595  rnghmval  45701  isrnghm  45702  lidlmsgrp  45736  lidlrng  45737  dmatALTbasel  45995  lindslinindsimp2  46056  lmod1  46085  isnrm4  46476  iscnrm4  46500  isthinc  46554  thincciso  46582