Theorem 2ralbidv 3018

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946

This theorem is referenced by:  cbvral3v  3211  ralxpxfr2d  3358  poeq1  5067  soeq1  5083  isoeq1  6607  isoeq2  6608  isoeq3  6609  fnmpt2ovd  7297  smoeq  7492  xpf1o  8163  nqereu  9789  dedekind  10238  dedekindle  10239  seqcaopr2  12877  wrd2ind  13523  addcn2  14368  mulcn2  14370  mreexexd  16355  mreexexdOLD  16356  catlid  16391  catrid  16392  isfunc  16571  funcres2b  16604  isfull  16617  isfth  16621  fullres2c  16646  isnat  16654  evlfcl  16909  uncfcurf  16926  isprs  16977  isdrs  16981  ispos  16994  istos  17082  isdlat  17240  sgrp1  17340  ismhm  17384  issubm  17394  sgrp2nmndlem4  17462  isnsg  17670  isghm  17707  isga  17770  pmtrdifwrdel  17951  sylow2blem2  18082  efglem  18175  efgi  18178  efgredlemb  18205  efgred  18207  frgpuplem  18231  iscmn  18246  ring1  18648  isirred  18745  islmod  18915  lmodlema  18916  lssset  18982  islssd  18984  islmhm  19075  islmhm2  19086  isobs  20112  dmatel  20347  dmatmulcl  20354  scmateALT  20366  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  cpmatel  20564  chpscmat  20695  hausnei2  21205  dfconn2  21270  llyeq  21321  nllyeq  21322  isucn2  22130  iducn  22134  ispsmet  22156  ismet  22175  isxmet  22176  metucn  22423  ngptgp  22487  nlmvscnlem1  22537  xmetdcn2  22687  addcnlem  22714  elcncf  22739  ipcnlem1  23090  cfili  23112  c1lip1  23805  aalioulem5  24136  aalioulem6  24137  aaliou  24138  aaliou2  24140  aaliou2b  24141  ulmcau  24194  ulmdvlem3  24201  cxpcn3lem  24533  dvdsmulf1o  24965  chpdifbndlem2  25288  pntrsumbnd2  25301  istrkgb  25399  axtgsegcon  25408  axtg5seg  25409  axtgpasch  25411  axtgeucl  25416  iscgrg  25452  isismt  25474  isperp2  25655  f1otrg  25796  axcontlem10  25898  axcontlem12  25900  isgrpo  27479  isablo  27528  vacn  27677  smcnlem  27680  lnoval  27735  islno  27736  isphg  27800  ajmoi  27842  ajval  27845  adjmo  28819  elcnop  28844  ellnop  28845  elunop  28859  elhmop  28860  elcnfn  28869  ellnfn  28870  adjeu  28876  adjval  28877  adj1  28920  adjeq  28922  cnlnadjlem9  29062  cnlnadjeu  29065  cnlnssadj  29067  isst  29200  ishst  29201  cdj1i  29420  cdj3i  29428  resspos  29787  resstos  29788  isomnd  29829  isslmd  29883  slmdlema  29884  isorng  29927  qqhucn  30164  ismntop  30198  axtgupdim2OLD  30874  txpconn  31340  nn0prpw  32443  heicant  33574  equivbnd  33719  isismty  33730  heibor1lem  33738  iccbnd  33769  isass  33775  elghomlem1OLD  33814  elghomlem2OLD  33815  isrngohom  33894  iscom2  33924  pridlval  33962  ispridl  33963  isdmn3  34003  inecmo  34260  islfl  34665  isopos  34785  psubspset  35348  islaut  35687  ispautN  35703  ltrnset  35722  isltrn  35723  istrnN  35762  istendo  36365  clsk1independent  38661  sprsymrelfolem2  42068  sprsymrelfo  42072  ismgmhm  42108  issubmgm  42114  isrnghm  42217  lidlmsgrp  42251  lidlrng  42252  dmatALTbasel  42516  lindslinindsimp2  42577  lmod1  42606