Theorem 2ralbidv 3235

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  3ralbidv  3238  6ralbidv  3240  cbvral3vw  3255  cbvral6vw  3257  cbvral3v  3366  rspc6v  3611  ralxpxfr2d  3614  poeq1  5573  soeq1  5591  isoeq1  7316  isoeq2  7317  isoeq3  7318  fnmpoovd  8082  xpord3inddlem  8150  smoeq  8337  xpf1o  9127  nqereu  10914  dedekind  11373  dedekindle  11374  seqcaopr2  14074  wrd2ind  14760  addcn2  15645  mulcn2  15647  mreexexd  17704  catlid  17739  catrid  17740  isfunc  17921  funcres2b  17954  isfull  17969  isfth  17973  fullres2c  17998  isnat  18007  evlfcl  18278  uncfcurf  18295  isprs  18352  isdrs  18357  ispos  18370  istos  18472  resspos  18485  resstos  18486  isdlat  18578  ismgmhm  18754  issubmgm  18760  sgrp1  18787  ismhm  18843  issubm  18861  sgrp2nmndlem4  18990  isnsg  19221  isghm  19286  isga  19361  pmtrdifwrdel  19555  sylow2blem2  19691  efglem  19786  efgi  19789  efgredlemb  19816  efgred  19818  frgpuplem  19842  iscmn  19859  isomnd  20193  ring1  20393  isirred  20501  rnghmval  20522  isrnghm  20523  isorng  20942  islmod  20963  lmodlema  20964  lssset  21032  islssd  21034  islmhm  21126  islmhm2  21137  prmidlval  21433  isprmidl  21434  isobs  21839  dmatel  22619  dmatmulcl  22626  scmateALT  22638  mdetunilem3  22740  mdetunilem4  22741  mdetunilem9  22746  cpmatel  22837  chpscmat  22968  hausnei2  23479  dfconn2  23545  llyeq  23596  nllyeq  23597  isucn2  24404  iducn  24408  ispsmet  24430  ismet  24449  isxmet  24450  metucn  24697  ngptgp  24762  nlmvscnlem1  24812  xmetdcn2  24964  addcnlem  24991  elcncf  25017  ipcnlem1  25373  cfili  25396  c1lip1  26125  aalioulem5  26466  aalioulem6  26467  aaliou  26468  aaliou2  26470  aaliou2b  26471  ulmcau  26524  ulmdvlem3  26531  cxpcn3lem  26878  mpodvdsmulf1o  27324  dvdsmulf1o  27326  chpdifbndlem2  27684  pntrsumbnd2  27697  addsprop  28135  negsprop  28194  istrkgb  28690  axtgsegcon  28699  axtg5seg  28700  axtgpasch  28702  axtgeucl  28707  iscgrg  28747  isismt  28769  isperp2  28954  f1otrg  29161  axcontlem10  29264  axcontlem12  29266  iscusgredg  29714  isgrpo  30790  isablo  30839  vacn  30987  smcnlem  30990  lnoval  31045  islno  31046  isphg  31110  ajmoi  31151  ajval  31154  adjmo  32125  elcnop  32150  ellnop  32151  elunop  32165  elhmop  32166  elcnfn  32175  ellnfn  32176  adjeu  32182  adjval  32183  adj1  32226  adjeq  32228  cnlnadjlem9  32368  cnlnadjeu  32371  cnlnssadj  32373  isst  32506  ishst  32507  cdj1i  32726  cdj3i  32734  ismnt  33244  mgcval  33248  isslmd  33463  slmdlema  33464  isrprm  33752  qqhucn  34327  ismntop  34361  axtgupdim2ALTV  35000  txpconn  35657  nmulprop  36615  nmulr0  36620  nn0prpw  36757  heicant  38228  equivbnd  38363  isismty  38374  heibor1lem  38382  iccbnd  38413  isass  38419  elghomlem1OLD  38458  elghomlem2OLD  38459  isrngohom  38538  iscom2  38568  pridlval  38606  ispridl  38607  isdmn3  38647  inecmo  38928  islfl  39758  isopos  39878  psubspset  40442  islaut  40781  ispautN  40797  ltrnset  40816  isltrn  40817  istrnN  40855  istendo  41458  sticksstones1  42837  sticksstones2  42838  sticksstones3  42839  sticksstones8  42844  sticksstones10  42846  sticksstones11  42847  sticksstones12a  42848  sticksstones15  42852  sn-isghm  43331  clsk1independent  44698  relpeq1  45579  relpeq2  45580  relpeq3  45581  sprsymrelfolem2  48165  sprsymrelfo  48169  reuopreuprim  48198  dmatALTbasel  49101  lindslinindsimp2  49162  lmod1  49191  isnrm4  49628  iscnrm4  49651  isuplem  49876  isthinc  50116  thincciso  50150  thinccisod  50151