Theorem 2ralbidv 2989

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

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  cbvral3v  3181  ralxpxfr2d  3327  poeq1  5038  soeq1  5054  isoeq1  6567  isoeq2  6568  isoeq3  6569  fnmpt2ovd  7252  smoeq  7447  xpf1o  8122  nqereu  9751  dedekind  10200  dedekindle  10201  seqcaopr2  12837  wrd2ind  13477  addcn2  14324  mulcn2  14326  mreexexd  16308  mreexexdOLD  16309  catlid  16344  catrid  16345  isfunc  16524  funcres2b  16557  isfull  16570  isfth  16574  fullres2c  16599  isnat  16607  evlfcl  16862  uncfcurf  16879  isprs  16930  isdrs  16934  ispos  16947  istos  17035  isdlat  17193  sgrp1  17293  ismhm  17337  issubm  17347  sgrp2nmndlem4  17415  isnsg  17623  isghm  17660  isga  17724  pmtrdifwrdel  17905  sylow2blem2  18036  efglem  18129  efgi  18132  efgredlemb  18159  efgred  18161  frgpuplem  18185  iscmn  18200  ring1  18602  isirred  18699  islmod  18867  lmodlema  18868  lssset  18934  islssd  18936  islmhm  19027  islmhm2  19038  isobs  20064  dmatel  20299  dmatmulcl  20306  scmateALT  20318  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  cpmatel  20516  chpscmat  20647  hausnei2  21157  dfconn2  21222  llyeq  21273  nllyeq  21274  isucn2  22083  iducn  22087  ispsmet  22109  ismet  22128  isxmet  22129  metucn  22376  ngptgp  22440  nlmvscnlem1  22490  xmetdcn2  22640  addcnlem  22667  elcncf  22692  ipcnlem1  23044  cfili  23066  c1lip1  23760  aalioulem5  24091  aalioulem6  24092  aaliou  24093  aaliou2  24095  aaliou2b  24096  ulmcau  24149  ulmdvlem3  24156  cxpcn3lem  24488  dvdsmulf1o  24920  chpdifbndlem2  25243  pntrsumbnd2  25256  istrkgb  25354  axtgsegcon  25363  axtg5seg  25364  axtgpasch  25366  axtgeucl  25371  iscgrg  25407  isismt  25429  isperp2  25610  f1otrg  25751  axcontlem10  25853  axcontlem12  25855  isgrpo  27351  isablo  27400  vacn  27549  smcnlem  27552  lnoval  27607  islno  27608  isphg  27672  ajmoi  27714  ajval  27717  adjmo  28691  elcnop  28716  ellnop  28717  elunop  28731  elhmop  28732  elcnfn  28741  ellnfn  28742  adjeu  28748  adjval  28749  adj1  28792  adjeq  28794  cnlnadjlem9  28934  cnlnadjeu  28937  cnlnssadj  28939  isst  29072  ishst  29073  cdj1i  29292  cdj3i  29300  resspos  29659  resstos  29660  isomnd  29701  isslmd  29755  slmdlema  29756  isorng  29799  qqhucn  30036  ismntop  30070  axtgupdim2OLD  30746  txpconn  31214  nn0prpw  32318  heicant  33444  equivbnd  33589  isismty  33600  heibor1lem  33608  iccbnd  33639  isass  33645  elghomlem1OLD  33684  elghomlem2OLD  33685  isrngohom  33764  iscom2  33794  pridlval  33832  ispridl  33833  isdmn3  33873  inecmo  34120  islfl  34347  isopos  34467  psubspset  35030  islaut  35369  ispautN  35385  ltrnset  35404  isltrn  35405  istrnN  35444  istendo  36048  clsk1independent  38344  sprsymrelfolem2  41743  sprsymrelfo  41747  ismgmhm  41783  issubmgm  41789  isrnghm  41892  lidlmsgrp  41926  lidlrng  41927  dmatALTbasel  42191  lindslinindsimp2  42252  lmod1  42281