Theorem 2ralbidv 3136

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

Syntax hints:   → wi 4   ↔ wb 197  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-an 385  df-ral 3060

This theorem is referenced by:  cbvral3v  3329  ralxpxfr2d  3481  poeq1  5203  soeq1  5219  isoeq1  6763  isoeq2  6764  isoeq3  6765  fnmpt2ovd  7457  fnmpt2ovdOLD  7458  smoeq  7655  xpf1o  8333  nqereu  10008  dedekind  10458  dedekindle  10459  seqcaopr2  13049  wrd2ind  13736  wrd2indOLD  13737  addcn2  14623  mulcn2  14625  mreexexd  16588  catlid  16623  catrid  16624  isfunc  16803  funcres2b  16836  isfull  16849  isfth  16853  fullres2c  16878  isnat  16886  evlfcl  17142  uncfcurf  17159  isprs  17210  isdrs  17214  ispos  17227  istos  17315  isdlat  17473  sgrp1  17573  ismhm  17617  issubm  17627  sgrp2nmndlem4  17696  isnsg  17901  isghm  17938  isga  18001  pmtrdifwrdel  18182  sylow2blem2  18314  efglem  18407  efgi  18410  efgredlemb  18438  efgred  18441  frgpuplem  18465  iscmn  18480  ring1  18883  isirred  18980  islmod  19150  lmodlema  19151  lssset  19217  islssd  19219  islmhm  19313  islmhm2  19324  isobs  20354  dmatel  20590  dmatmulcl  20597  scmateALT  20609  mdetunilem3  20711  mdetunilem4  20712  mdetunilem9  20717  cpmatel  20809  chpscmat  20940  hausnei2  21451  dfconn2  21516  llyeq  21567  nllyeq  21568  isucn2  22376  iducn  22380  ispsmet  22402  ismet  22421  isxmet  22422  metucn  22669  ngptgp  22733  nlmvscnlem1  22783  xmetdcn2  22933  addcnlem  22960  elcncf  22985  ipcnlem1  23336  cfili  23359  c1lip1  24065  aalioulem5  24396  aalioulem6  24397  aaliou  24398  aaliou2  24400  aaliou2b  24401  ulmcau  24454  ulmdvlem3  24461  cxpcn3lem  24793  dvdsmulf1o  25225  chpdifbndlem2  25548  pntrsumbnd2  25561  istrkgb  25659  axtgsegcon  25668  axtg5seg  25669  axtgpasch  25671  axtgeucl  25676  iscgrg  25712  isismt  25734  isperp2  25915  f1otrg  26056  axcontlem10  26158  axcontlem12  26160  isgrpo  27829  isablo  27878  vacn  28026  smcnlem  28029  lnoval  28084  islno  28085  isphg  28149  ajmoi  28191  ajval  28194  adjmo  29168  elcnop  29193  ellnop  29194  elunop  29208  elhmop  29209  elcnfn  29218  ellnfn  29219  adjeu  29225  adjval  29226  adj1  29269  adjeq  29271  cnlnadjlem9  29411  cnlnadjeu  29414  cnlnssadj  29416  isst  29549  ishst  29550  cdj1i  29769  cdj3i  29777  resspos  30127  resstos  30128  isomnd  30169  isslmd  30223  slmdlema  30224  isorng  30267  qqhucn  30504  ismntop  30538  axtgupdim2OLD  31218  txpconn  31683  nn0prpw  32782  heicant  33889  equivbnd  34032  isismty  34043  heibor1lem  34051  iccbnd  34082  isass  34088  elghomlem1OLD  34127  elghomlem2OLD  34128  isrngohom  34207  iscom2  34237  pridlval  34275  ispridl  34276  isdmn3  34316  inecmo  34570  islfl  35037  isopos  35157  psubspset  35721  islaut  36060  ispautN  36076  ltrnset  36095  isltrn  36096  istrnN  36134  istendo  36737  clsk1independent  39042  sprsymrelfolem2  42436  sprsymrelfo  42440  ismgmhm  42476  issubmgm  42482  isrnghm  42585  lidlmsgrp  42619  lidlrng  42620  dmatALTbasel  42884  lindslinindsimp2  42945  lmod1  42974