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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  3ralbidv  3202  6ralbidv  3204  cbvral3vw  3219  cbvral6vw  3221  cbvral3v  3341  rspc6v  3606  ralxpxfr2d  3609  poeq1  5542  soeq1  5560  isoeq1  7274  isoeq2  7275  isoeq3  7276  fnmpoovd  8043  xpord3inddlem  8110  smoeq  8296  xpf1o  9080  nqereu  10858  dedekind  11313  dedekindle  11314  seqcaopr2  13979  wrd2ind  14664  addcn2  15536  mulcn2  15538  mreexexd  17589  catlid  17624  catrid  17625  isfunc  17806  funcres2b  17839  isfull  17854  isfth  17858  fullres2c  17883  isnat  17892  evlfcl  18163  uncfcurf  18180  isprs  18237  isdrs  18242  ispos  18255  istos  18357  resspos  18370  resstos  18371  isdlat  18463  ismgmhm  18605  issubmgm  18611  sgrp1  18638  ismhm  18694  issubm  18712  sgrp2nmndlem4  18837  isnsg  19069  isghm  19129  isghmOLD  19130  isga  19205  pmtrdifwrdel  19399  sylow2blem2  19535  efglem  19630  efgi  19633  efgredlemb  19660  efgred  19662  frgpuplem  19686  iscmn  19703  isomnd  20037  ring1  20230  isirred  20339  rnghmval  20360  isrnghm  20361  isorng  20781  islmod  20802  lmodlema  20803  lssset  20871  islssd  20873  islmhm  20966  islmhm2  20977  isobs  21662  dmatel  22413  dmatmulcl  22420  scmateALT  22432  mdetunilem3  22534  mdetunilem4  22535  mdetunilem9  22540  cpmatel  22631  chpscmat  22762  hausnei2  23273  dfconn2  23339  llyeq  23390  nllyeq  23391  isucn2  24199  iducn  24203  ispsmet  24225  ismet  24244  isxmet  24245  metucn  24492  ngptgp  24557  nlmvscnlem1  24607  xmetdcn2  24759  addcnlem  24786  elcncf  24815  ipcnlem1  25178  cfili  25201  c1lip1  25935  aalioulem5  26277  aalioulem6  26278  aaliou  26279  aaliou2  26281  aaliou2b  26282  ulmcau  26337  ulmdvlem3  26344  cxpcn3lem  26690  mpodvdsmulf1o  27137  dvdsmulf1o  27139  chpdifbndlem2  27498  pntrsumbnd2  27511  addsprop  27923  negsprop  27981  istrkgb  28435  axtgsegcon  28444  axtg5seg  28445  axtgpasch  28447  axtgeucl  28452  iscgrg  28492  isismt  28514  isperp2  28695  f1otrg  28851  axcontlem10  28953  axcontlem12  28955  iscusgredg  29403  isgrpo  30476  isablo  30525  vacn  30673  smcnlem  30676  lnoval  30731  islno  30732  isphg  30796  ajmoi  30837  ajval  30840  adjmo  31811  elcnop  31836  ellnop  31837  elunop  31851  elhmop  31852  elcnfn  31861  ellnfn  31862  adjeu  31868  adjval  31869  adj1  31912  adjeq  31914  cnlnadjlem9  32054  cnlnadjeu  32057  cnlnssadj  32059  isst  32192  ishst  32193  cdj1i  32412  cdj3i  32420  ismnt  32955  mgcval  32959  isslmd  33171  slmdlema  33172  prmidlval  33401  isprmidl  33402  isrprm  33481  qqhucn  33975  ismntop  34009  axtgupdim2ALTV  34652  txpconn  35212  nn0prpw  36304  heicant  37642  equivbnd  37777  isismty  37788  heibor1lem  37796  iccbnd  37827  isass  37833  elghomlem1OLD  37872  elghomlem2OLD  37873  isrngohom  37952  iscom2  37982  pridlval  38020  ispridl  38021  isdmn3  38061  inecmo  38330  islfl  39046  isopos  39166  psubspset  39731  islaut  40070  ispautN  40086  ltrnset  40105  isltrn  40106  istrnN  40144  istendo  40747  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones15  42142  sn-isghm  42654  clsk1independent  44028  relpeq1  44927  relpeq2  44928  relpeq3  44929  sprsymrelfolem2  47487  sprsymrelfo  47491  reuopreuprim  47520  dmatALTbasel  48384  lindslinindsimp2  48445  lmod1  48474  isnrm4  48912  iscnrm4  48935  isuplem  49161  isthinc  49401  thincciso  49435  thinccisod  49436