Theorem 2ralbidv 3168

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3107

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3112

This theorem is referenced by:  cbvral3v  3416  ralxpxfr2d  3580  poeq1  5372  soeq1  5389  isoeq1  6940  isoeq2  6941  isoeq3  6942  fnmpoovd  7645  smoeq  7846  xpf1o  8533  nqereu  10204  dedekind  10656  dedekindle  10657  seqcaopr2  13260  wrd2ind  13925  addcn2  14788  mulcn2  14790  mreexexd  16752  catlid  16787  catrid  16788  isfunc  16967  funcres2b  17000  isfull  17013  isfth  17017  fullres2c  17042  isnat  17050  evlfcl  17305  uncfcurf  17322  isprs  17373  isdrs  17377  ispos  17390  istos  17478  isdlat  17636  sgrp1  17736  ismhm  17780  issubm  17790  sgrp2nmndlem4  17858  isnsg  18066  isghm  18103  isga  18166  pmtrdifwrdel  18348  sylow2blem2  18480  efglem  18573  efgi  18576  efgredlemb  18603  efgred  18605  frgpuplem  18629  iscmn  18644  ring1  19046  isirred  19143  islmod  19332  lmodlema  19333  lssset  19399  islssd  19401  islmhm  19493  islmhm2  19504  isobs  20550  dmatel  20790  dmatmulcl  20797  scmateALT  20809  mdetunilem3  20911  mdetunilem4  20912  mdetunilem9  20917  cpmatel  21007  chpscmat  21138  hausnei2  21649  dfconn2  21715  llyeq  21766  nllyeq  21767  isucn2  22575  iducn  22579  ispsmet  22601  ismet  22620  isxmet  22621  metucn  22868  ngptgp  22932  nlmvscnlem1  22982  xmetdcn2  23132  addcnlem  23159  elcncf  23184  ipcnlem1  23535  cfili  23558  c1lip1  24281  aalioulem5  24612  aalioulem6  24613  aaliou  24614  aaliou2  24616  aaliou2b  24617  ulmcau  24670  ulmdvlem3  24677  cxpcn3lem  25013  dvdsmulf1o  25457  chpdifbndlem2  25816  pntrsumbnd2  25829  istrkgb  25927  axtgsegcon  25936  axtg5seg  25937  axtgpasch  25939  axtgeucl  25944  iscgrg  25984  isismt  26006  isperp2  26187  f1otrg  26344  axcontlem10  26446  axcontlem12  26448  iscusgredg  26892  isgrpo  27961  isablo  28010  vacn  28158  smcnlem  28161  lnoval  28216  islno  28217  isphg  28281  ajmoi  28322  ajval  28325  adjmo  29296  elcnop  29321  ellnop  29322  elunop  29336  elhmop  29337  elcnfn  29346  ellnfn  29347  adjeu  29353  adjval  29354  adj1  29397  adjeq  29399  cnlnadjlem9  29539  cnlnadjeu  29542  cnlnssadj  29544  isst  29677  ishst  29678  cdj1i  29897  cdj3i  29905  resspos  30316  resstos  30317  isomnd  30358  isslmd  30464  slmdlema  30465  isorng  30522  qqhucn  30846  ismntop  30880  axtgupdim2ALTV  31552  txpconn  32089  nn0prpw  33282  heicant  34479  equivbnd  34621  isismty  34632  heibor1lem  34640  iccbnd  34671  isass  34677  elghomlem1OLD  34716  elghomlem2OLD  34717  isrngohom  34796  iscom2  34826  pridlval  34864  ispridl  34865  isdmn3  34905  inecmo  35162  islfl  35748  isopos  35868  psubspset  36432  islaut  36771  ispautN  36787  ltrnset  36806  isltrn  36807  istrnN  36845  istendo  37448  clsk1independent  39902  sprsymrelfolem2  43159  sprsymrelfo  43163  reuopreuprim  43192  ismgmhm  43554  issubmgm  43560  rnghmval  43662  isrnghm  43663  lidlmsgrp  43697  lidlrng  43698  dmatALTbasel  43959  lindslinindsimp2  44020  lmod1  44049