Theorem 2ralbidv 3199

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  cbvral3vw  3464  cbvral3v  3467  ralxpxfr2d  3639  poeq1  5472  soeq1  5489  isoeq1  7064  isoeq2  7065  isoeq3  7066  fnmpoovd  7776  smoeq  7981  xpf1o  8673  nqereu  10345  dedekind  10797  dedekindle  10798  seqcaopr2  13400  wrd2ind  14079  addcn2  14944  mulcn2  14946  mreexexd  16913  catlid  16948  catrid  16949  isfunc  17128  funcres2b  17161  isfull  17174  isfth  17178  fullres2c  17203  isnat  17211  evlfcl  17466  uncfcurf  17483  isprs  17534  isdrs  17538  ispos  17551  istos  17639  isdlat  17797  sgrp1  17904  ismhm  17952  issubm  17962  sgrp2nmndlem4  18087  isnsg  18301  isghm  18352  isga  18415  pmtrdifwrdel  18607  sylow2blem2  18740  efglem  18836  efgi  18839  efgredlemb  18866  efgred  18868  frgpuplem  18892  iscmn  18908  ring1  19346  isirred  19443  islmod  19632  lmodlema  19633  lssset  19699  islssd  19701  islmhm  19793  islmhm2  19804  isobs  20858  dmatel  21096  dmatmulcl  21103  scmateALT  21115  mdetunilem3  21217  mdetunilem4  21218  mdetunilem9  21223  cpmatel  21313  chpscmat  21444  hausnei2  21955  dfconn2  22021  llyeq  22072  nllyeq  22073  isucn2  22882  iducn  22886  ispsmet  22908  ismet  22927  isxmet  22928  metucn  23175  ngptgp  23239  nlmvscnlem1  23289  xmetdcn2  23439  addcnlem  23466  elcncf  23491  ipcnlem1  23842  cfili  23865  c1lip1  24588  aalioulem5  24919  aalioulem6  24920  aaliou  24921  aaliou2  24923  aaliou2b  24924  ulmcau  24977  ulmdvlem3  24984  cxpcn3lem  25322  dvdsmulf1o  25765  chpdifbndlem2  26124  pntrsumbnd2  26137  istrkgb  26235  axtgsegcon  26244  axtg5seg  26245  axtgpasch  26247  axtgeucl  26252  iscgrg  26292  isismt  26314  isperp2  26495  f1otrg  26651  axcontlem10  26753  axcontlem12  26755  iscusgredg  27199  isgrpo  28268  isablo  28317  vacn  28465  smcnlem  28468  lnoval  28523  islno  28524  isphg  28588  ajmoi  28629  ajval  28632  adjmo  29603  elcnop  29628  ellnop  29629  elunop  29643  elhmop  29644  elcnfn  29653  ellnfn  29654  adjeu  29660  adjval  29661  adj1  29704  adjeq  29706  cnlnadjlem9  29846  cnlnadjeu  29849  cnlnssadj  29851  isst  29984  ishst  29985  cdj1i  30204  cdj3i  30212  resspos  30641  resstos  30642  isomnd  30697  isslmd  30825  slmdlema  30826  isorng  30867  prmidlval  30949  isprmidl  30950  qqhucn  31228  ismntop  31262  axtgupdim2ALTV  31934  txpconn  32474  nn0prpw  33666  heicant  34921  equivbnd  35062  isismty  35073  heibor1lem  35081  iccbnd  35112  isass  35118  elghomlem1OLD  35157  elghomlem2OLD  35158  isrngohom  35237  iscom2  35267  pridlval  35305  ispridl  35306  isdmn3  35346  inecmo  35603  islfl  36190  isopos  36310  psubspset  36874  islaut  37213  ispautN  37229  ltrnset  37248  isltrn  37249  istrnN  37287  istendo  37890  clsk1independent  40389  sprsymrelfolem2  43648  sprsymrelfo  43652  reuopreuprim  43681  ismgmhm  44043  issubmgm  44049  rnghmval  44155  isrnghm  44156  lidlmsgrp  44190  lidlrng  44191  dmatALTbasel  44450  lindslinindsimp2  44511  lmod1  44540