Theorem 2ralbidv 3201

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  cbvral3vw  3465  cbvral3v  3468  ralxpxfr2d  3641  poeq1  5479  soeq1  5496  isoeq1  7072  isoeq2  7073  isoeq3  7074  fnmpoovd  7784  smoeq  7989  xpf1o  8681  nqereu  10353  dedekind  10805  dedekindle  10806  seqcaopr2  13409  wrd2ind  14087  addcn2  14952  mulcn2  14954  mreexexd  16921  catlid  16956  catrid  16957  isfunc  17136  funcres2b  17169  isfull  17182  isfth  17186  fullres2c  17211  isnat  17219  evlfcl  17474  uncfcurf  17491  isprs  17542  isdrs  17546  ispos  17559  istos  17647  isdlat  17805  sgrp1  17912  ismhm  17960  issubm  17970  sgrp2nmndlem4  18095  isnsg  18309  isghm  18360  isga  18423  pmtrdifwrdel  18615  sylow2blem2  18748  efglem  18844  efgi  18847  efgredlemb  18874  efgred  18876  frgpuplem  18900  iscmn  18916  ring1  19354  isirred  19451  islmod  19640  lmodlema  19641  lssset  19707  islssd  19709  islmhm  19801  islmhm2  19812  isobs  20866  dmatel  21104  dmatmulcl  21111  scmateALT  21123  mdetunilem3  21225  mdetunilem4  21226  mdetunilem9  21231  cpmatel  21321  chpscmat  21452  hausnei2  21963  dfconn2  22029  llyeq  22080  nllyeq  22081  isucn2  22890  iducn  22894  ispsmet  22916  ismet  22935  isxmet  22936  metucn  23183  ngptgp  23247  nlmvscnlem1  23297  xmetdcn2  23447  addcnlem  23474  elcncf  23499  ipcnlem1  23850  cfili  23873  c1lip1  24596  aalioulem5  24927  aalioulem6  24928  aaliou  24929  aaliou2  24931  aaliou2b  24932  ulmcau  24985  ulmdvlem3  24992  cxpcn3lem  25330  dvdsmulf1o  25773  chpdifbndlem2  26132  pntrsumbnd2  26145  istrkgb  26243  axtgsegcon  26252  axtg5seg  26253  axtgpasch  26255  axtgeucl  26260  iscgrg  26300  isismt  26322  isperp2  26503  f1otrg  26659  axcontlem10  26761  axcontlem12  26763  iscusgredg  27207  isgrpo  28276  isablo  28325  vacn  28473  smcnlem  28476  lnoval  28531  islno  28532  isphg  28596  ajmoi  28637  ajval  28640  adjmo  29611  elcnop  29636  ellnop  29637  elunop  29651  elhmop  29652  elcnfn  29661  ellnfn  29662  adjeu  29668  adjval  29669  adj1  29712  adjeq  29714  cnlnadjlem9  29854  cnlnadjeu  29857  cnlnssadj  29859  isst  29992  ishst  29993  cdj1i  30212  cdj3i  30220  resspos  30648  resstos  30649  isomnd  30704  isslmd  30832  slmdlema  30833  isorng  30874  prmidlval  30956  isprmidl  30957  qqhucn  31235  ismntop  31269  axtgupdim2ALTV  31941  txpconn  32481  nn0prpw  33673  heicant  34929  equivbnd  35070  isismty  35081  heibor1lem  35089  iccbnd  35120  isass  35126  elghomlem1OLD  35165  elghomlem2OLD  35166  isrngohom  35245  iscom2  35275  pridlval  35313  ispridl  35314  isdmn3  35354  inecmo  35611  islfl  36198  isopos  36318  psubspset  36882  islaut  37221  ispautN  37237  ltrnset  37256  isltrn  37257  istrnN  37295  istendo  37898  clsk1independent  40403  sprsymrelfolem2  43662  sprsymrelfo  43666  reuopreuprim  43695  ismgmhm  44057  issubmgm  44063  rnghmval  44169  isrnghm  44170  lidlmsgrp  44204  lidlrng  44205  dmatALTbasel  44464  lindslinindsimp2  44525  lmod1  44554