Theorem 2ralbidv 2972

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (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 2969	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 2969	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 195  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  cbvral3v  3157  ralxpxfr2d  3298  poeq1  4962  soeq1  4978  isoeq1  6467  isoeq2  6468  isoeq3  6469  fnmpt2ovd  7139  smoeq  7334  xpf1o  8007  nqereu  9630  dedekind  10079  dedekindle  10080  seqcaopr2  12699  wrd2ind  13329  addcn2  14172  mulcn2  14174  mreexexd  16131  mreexexdOLD  16132  catlid  16167  catrid  16168  isfunc  16347  funcres2b  16380  isfull  16393  isfth  16397  fullres2c  16422  isnat  16430  evlfcl  16685  uncfcurf  16702  isprs  16753  isdrs  16757  ispos  16770  istos  16858  isdlat  17016  sgrp1  17116  ismhm  17160  issubm  17170  sgrp2nmndlem4  17238  isnsg  17446  isghm  17483  isga  17547  pmtrdifwrdel  17728  sylow2blem2  17859  efglem  17952  efgi  17955  efgredlemb  17982  efgred  17984  frgpuplem  18008  iscmn  18023  ring1  18425  isirred  18522  islmod  18690  lmodlema  18691  lssset  18755  islssd  18757  islmhm  18848  islmhm2  18859  isobs  19883  dmatel  20118  dmatmulcl  20125  scmateALT  20137  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  cpmatel  20335  chpscmat  20466  hausnei2  20967  dfcon2  21032  llyeq  21083  nllyeq  21084  isucn2  21893  iducn  21897  ispsmet  21919  ismet  21938  isxmet  21939  metucn  22186  ngptgp  22250  nlmvscnlem1  22300  xmetdcn2  22448  addcnlem  22475  elcncf  22500  ipcnlem1  22852  cfili  22874  c1lip1  23564  aalioulem5  23895  aalioulem6  23896  aaliou  23897  aaliou2  23899  aaliou2b  23900  ulmcau  23953  ulmdvlem3  23960  cxpcn3lem  24288  dvdsmulf1o  24720  chpdifbndlem2  25043  pntrsumbnd2  25056  istrkgb  25154  axtgsegcon  25163  axtg5seg  25164  axtgpasch  25166  axtgeucl  25171  iscgrg  25207  isismt  25229  isperp2  25410  f1otrg  25551  axcontlem10  25653  axcontlem12  25655  isfrgra  26517  isgrpo  26735  isablo  26784  vacn  26933  smcnlem  26936  lnoval  26991  islno  26992  isphg  27056  ajmoi  27098  ajval  27101  adjmo  28075  elcnop  28100  ellnop  28101  elunop  28115  elhmop  28116  elcnfn  28125  ellnfn  28126  adjeu  28132  adjval  28133  adj1  28176  adjeq  28178  cnlnadjlem9  28318  cnlnadjeu  28321  cnlnssadj  28323  isst  28456  ishst  28457  cdj1i  28676  cdj3i  28684  resspos  28990  resstos  28991  isomnd  29032  isslmd  29086  slmdlema  29087  isorng  29130  qqhucn  29364  ismntop  29398  axtgupdim2OLD  29999  txpcon  30468  nofulllem4  31104  nofulllem5  31105  nn0prpw  31488  heicant  32614  equivbnd  32759  isismty  32770  heibor1lem  32778  iccbnd  32809  isass  32815  elghomlem1OLD  32854  elghomlem2OLD  32855  isrngohom  32934  iscom2  32964  pridlval  33002  ispridl  33003  isdmn3  33043  islfl  33365  isopos  33485  psubspset  34048  islaut  34387  ispautN  34403  ltrnset  34422  isltrn  34423  istrnN  34462  istendo  35066  clsk1independent  37364  ismgmhm  41573  issubmgm  41579  isrnghm  41682  lidlmsgrp  41716  lidlrng  41717  dmatALTbasel  41985  lindslinindsimp2  42046  lmod1  42075