Theorem 2ralbidv 3202

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  3ralbidv  3205  6ralbidv  3207  cbvral3vw  3222  cbvral6vw  3224  cbvral3v  3333  rspc6v  3586  ralxpxfr2d  3589  poeq1  5537  soeq1  5555  isoeq1  7267  isoeq2  7268  isoeq3  7269  fnmpoovd  8032  xpord3inddlem  8099  smoeq  8285  xpf1o  9072  nqereu  10847  dedekind  11304  dedekindle  11305  seqcaopr2  13995  wrd2ind  14680  addcn2  15551  mulcn2  15553  mreexexd  17609  catlid  17644  catrid  17645  isfunc  17826  funcres2b  17859  isfull  17874  isfth  17878  fullres2c  17903  isnat  17912  evlfcl  18183  uncfcurf  18200  isprs  18257  isdrs  18262  ispos  18275  istos  18377  resspos  18390  resstos  18391  isdlat  18483  ismgmhm  18659  issubmgm  18665  sgrp1  18692  ismhm  18748  issubm  18766  sgrp2nmndlem4  18894  isnsg  19125  isghm  19185  isghmOLD  19186  isga  19261  pmtrdifwrdel  19455  sylow2blem2  19591  efglem  19686  efgi  19689  efgredlemb  19716  efgred  19718  frgpuplem  19742  iscmn  19759  isomnd  20093  ring1  20286  isirred  20394  rnghmval  20415  isrnghm  20416  isorng  20833  islmod  20854  lmodlema  20855  lssset  20923  islssd  20925  islmhm  21018  islmhm2  21029  isobs  21714  dmatel  22472  dmatmulcl  22479  scmateALT  22491  mdetunilem3  22593  mdetunilem4  22594  mdetunilem9  22599  cpmatel  22690  chpscmat  22821  hausnei2  23332  dfconn2  23398  llyeq  23449  nllyeq  23450  isucn2  24257  iducn  24261  ispsmet  24283  ismet  24302  isxmet  24303  metucn  24550  ngptgp  24615  nlmvscnlem1  24665  xmetdcn2  24817  addcnlem  24844  elcncf  24870  ipcnlem1  25226  cfili  25249  c1lip1  25978  aalioulem5  26317  aalioulem6  26318  aaliou  26319  aaliou2  26321  aaliou2b  26322  ulmcau  26377  ulmdvlem3  26384  cxpcn3lem  26728  mpodvdsmulf1o  27175  dvdsmulf1o  27177  chpdifbndlem2  27535  pntrsumbnd2  27548  addsprop  27986  negsprop  28045  istrkgb  28541  axtgsegcon  28550  axtg5seg  28551  axtgpasch  28553  axtgeucl  28558  iscgrg  28598  isismt  28620  isperp2  28801  f1otrg  28957  axcontlem10  29060  axcontlem12  29062  iscusgredg  29510  isgrpo  30587  isablo  30636  vacn  30784  smcnlem  30787  lnoval  30842  islno  30843  isphg  30907  ajmoi  30948  ajval  30951  adjmo  31922  elcnop  31947  ellnop  31948  elunop  31962  elhmop  31963  elcnfn  31972  ellnfn  31973  adjeu  31979  adjval  31980  adj1  32023  adjeq  32025  cnlnadjlem9  32165  cnlnadjeu  32168  cnlnssadj  32170  isst  32303  ishst  32304  cdj1i  32523  cdj3i  32531  ismnt  33062  mgcval  33066  isslmd  33282  slmdlema  33283  prmidlval  33516  isprmidl  33517  isrprm  33596  qqhucn  34156  ismntop  34190  axtgupdim2ALTV  34832  txpconn  35434  nn0prpw  36525  heicant  37994  equivbnd  38129  isismty  38140  heibor1lem  38148  iccbnd  38179  isass  38185  elghomlem1OLD  38224  elghomlem2OLD  38225  isrngohom  38304  iscom2  38334  pridlval  38372  ispridl  38373  isdmn3  38413  inecmo  38694  islfl  39524  isopos  39644  psubspset  40208  islaut  40547  ispautN  40563  ltrnset  40582  isltrn  40583  istrnN  40621  istendo  41224  sticksstones1  42603  sticksstones2  42604  sticksstones3  42605  sticksstones8  42610  sticksstones10  42612  sticksstones11  42613  sticksstones12a  42614  sticksstones15  42618  sn-isghm  43124  clsk1independent  44495  relpeq1  45393  relpeq2  45394  relpeq3  45395  sprsymrelfolem2  47969  sprsymrelfo  47973  reuopreuprim  48002  dmatALTbasel  48894  lindslinindsimp2  48955  lmod1  48984  isnrm4  49422  iscnrm4  49445  isuplem  49670  isthinc  49910  thincciso  49944  thinccisod  49945