Theorem 2ralbidv 3205

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

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

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 3052

This theorem is referenced by:  3ralbidv  3208  6ralbidv  3210  cbvral3vw  3226  cbvral6vw  3228  cbvral3v  3349  rspc6v  3622  ralxpxfr2d  3625  poeq1  5564  soeq1  5582  isoeq1  7309  isoeq2  7310  isoeq3  7311  fnmpoovd  8084  xpord3inddlem  8151  smoeq  8362  xpf1o  9151  nqereu  10941  dedekind  11396  dedekindle  11397  seqcaopr2  14054  wrd2ind  14739  addcn2  15608  mulcn2  15610  mreexexd  17658  catlid  17693  catrid  17694  isfunc  17875  funcres2b  17908  isfull  17923  isfth  17927  fullres2c  17952  isnat  17961  evlfcl  18232  uncfcurf  18249  isprs  18306  isdrs  18311  ispos  18324  istos  18426  isdlat  18530  ismgmhm  18672  issubmgm  18678  sgrp1  18705  ismhm  18761  issubm  18779  sgrp2nmndlem4  18904  isnsg  19136  isghm  19196  isghmOLD  19197  isga  19272  pmtrdifwrdel  19464  sylow2blem2  19600  efglem  19695  efgi  19698  efgredlemb  19725  efgred  19727  frgpuplem  19751  iscmn  19768  ring1  20268  isirred  20377  rnghmval  20398  isrnghm  20399  islmod  20819  lmodlema  20820  lssset  20888  islssd  20890  islmhm  20983  islmhm2  20994  isobs  21678  dmatel  22429  dmatmulcl  22436  scmateALT  22448  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  cpmatel  22647  chpscmat  22778  hausnei2  23289  dfconn2  23355  llyeq  23406  nllyeq  23407  isucn2  24215  iducn  24219  ispsmet  24241  ismet  24260  isxmet  24261  metucn  24508  ngptgp  24573  nlmvscnlem1  24623  xmetdcn2  24775  addcnlem  24802  elcncf  24831  ipcnlem1  25195  cfili  25218  c1lip1  25952  aalioulem5  26294  aalioulem6  26295  aaliou  26296  aaliou2  26298  aaliou2b  26299  ulmcau  26354  ulmdvlem3  26361  cxpcn3lem  26707  mpodvdsmulf1o  27154  dvdsmulf1o  27156  chpdifbndlem2  27515  pntrsumbnd2  27528  addsprop  27926  negsprop  27984  istrkgb  28380  axtgsegcon  28389  axtg5seg  28390  axtgpasch  28392  axtgeucl  28397  iscgrg  28437  isismt  28459  isperp2  28640  f1otrg  28796  axcontlem10  28898  axcontlem12  28900  iscusgredg  29348  isgrpo  30424  isablo  30473  vacn  30621  smcnlem  30624  lnoval  30679  islno  30680  isphg  30744  ajmoi  30785  ajval  30788  adjmo  31759  elcnop  31784  ellnop  31785  elunop  31799  elhmop  31800  elcnfn  31809  ellnfn  31810  adjeu  31816  adjval  31817  adj1  31860  adjeq  31862  cnlnadjlem9  32002  cnlnadjeu  32005  cnlnssadj  32007  isst  32140  ishst  32141  cdj1i  32360  cdj3i  32368  resspos  32892  resstos  32893  ismnt  32909  mgcval  32913  isomnd  33015  isslmd  33145  slmdlema  33146  isorng  33267  prmidlval  33398  isprmidl  33399  isrprm  33478  qqhucn  33969  ismntop  34003  axtgupdim2ALTV  34646  txpconn  35200  nn0prpw  36287  heicant  37625  equivbnd  37760  isismty  37771  heibor1lem  37779  iccbnd  37810  isass  37816  elghomlem1OLD  37855  elghomlem2OLD  37856  isrngohom  37935  iscom2  37965  pridlval  38003  ispridl  38004  isdmn3  38044  inecmo  38319  islfl  39024  isopos  39144  psubspset  39709  islaut  40048  ispautN  40064  ltrnset  40083  isltrn  40084  istrnN  40122  istendo  40725  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones8  42112  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones15  42120  sn-isghm  42643  clsk1independent  44017  relpeq1  44917  relpeq2  44918  relpeq3  44919  sprsymrelfolem2  47455  sprsymrelfo  47459  reuopreuprim  47488  dmatALTbasel  48326  lindslinindsimp2  48387  lmod1  48416  isnrm4  48853  iscnrm4  48876  isuplem  49062  isthinc  49253  thincciso  49287  thinccisod  49288