Theorem 2ralbidv 3193

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 3152	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 3152	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  3196  6ralbidv  3198  cbvral3vw  3213  cbvral6vw  3215  cbvral3v  3333  rspc6v  3598  ralxpxfr2d  3601  poeq1  5530  soeq1  5548  isoeq1  7254  isoeq2  7255  isoeq3  7256  fnmpoovd  8020  xpord3inddlem  8087  smoeq  8273  xpf1o  9056  nqereu  10823  dedekind  11279  dedekindle  11280  seqcaopr2  13945  wrd2ind  14629  addcn2  15501  mulcn2  15503  mreexexd  17554  catlid  17589  catrid  17590  isfunc  17771  funcres2b  17804  isfull  17819  isfth  17823  fullres2c  17848  isnat  17857  evlfcl  18128  uncfcurf  18145  isprs  18202  isdrs  18207  ispos  18220  istos  18322  resspos  18335  resstos  18336  isdlat  18428  ismgmhm  18570  issubmgm  18576  sgrp1  18603  ismhm  18659  issubm  18677  sgrp2nmndlem4  18802  isnsg  19034  isghm  19094  isghmOLD  19095  isga  19170  pmtrdifwrdel  19364  sylow2blem2  19500  efglem  19595  efgi  19598  efgredlemb  19625  efgred  19627  frgpuplem  19651  iscmn  19668  isomnd  20002  ring1  20195  isirred  20304  rnghmval  20325  isrnghm  20326  isorng  20746  islmod  20767  lmodlema  20768  lssset  20836  islssd  20838  islmhm  20931  islmhm2  20942  isobs  21627  dmatel  22378  dmatmulcl  22385  scmateALT  22397  mdetunilem3  22499  mdetunilem4  22500  mdetunilem9  22505  cpmatel  22596  chpscmat  22727  hausnei2  23238  dfconn2  23304  llyeq  23355  nllyeq  23356  isucn2  24164  iducn  24168  ispsmet  24190  ismet  24209  isxmet  24210  metucn  24457  ngptgp  24522  nlmvscnlem1  24572  xmetdcn2  24724  addcnlem  24751  elcncf  24780  ipcnlem1  25143  cfili  25166  c1lip1  25900  aalioulem5  26242  aalioulem6  26243  aaliou  26244  aaliou2  26246  aaliou2b  26247  ulmcau  26302  ulmdvlem3  26309  cxpcn3lem  26655  mpodvdsmulf1o  27102  dvdsmulf1o  27104  chpdifbndlem2  27463  pntrsumbnd2  27476  addsprop  27888  negsprop  27946  istrkgb  28400  axtgsegcon  28409  axtg5seg  28410  axtgpasch  28412  axtgeucl  28417  iscgrg  28457  isismt  28479  isperp2  28660  f1otrg  28816  axcontlem10  28918  axcontlem12  28920  iscusgredg  29368  isgrpo  30441  isablo  30490  vacn  30638  smcnlem  30641  lnoval  30696  islno  30697  isphg  30761  ajmoi  30802  ajval  30805  adjmo  31776  elcnop  31801  ellnop  31802  elunop  31816  elhmop  31817  elcnfn  31826  ellnfn  31827  adjeu  31833  adjval  31834  adj1  31877  adjeq  31879  cnlnadjlem9  32019  cnlnadjeu  32022  cnlnssadj  32024  isst  32157  ishst  32158  cdj1i  32377  cdj3i  32385  ismnt  32926  mgcval  32930  isslmd  33145  slmdlema  33146  prmidlval  33375  isprmidl  33376  isrprm  33455  qqhucn  33965  ismntop  33999  axtgupdim2ALTV  34642  txpconn  35215  nn0prpw  36307  heicant  37645  equivbnd  37780  isismty  37791  heibor1lem  37799  iccbnd  37830  isass  37836  elghomlem1OLD  37875  elghomlem2OLD  37876  isrngohom  37955  iscom2  37985  pridlval  38023  ispridl  38024  isdmn3  38064  inecmo  38333  islfl  39049  isopos  39169  psubspset  39733  islaut  40072  ispautN  40088  ltrnset  40107  isltrn  40108  istrnN  40146  istendo  40749  sticksstones1  42129  sticksstones2  42130  sticksstones3  42131  sticksstones8  42136  sticksstones10  42138  sticksstones11  42139  sticksstones12a  42140  sticksstones15  42144  sn-isghm  42656  clsk1independent  44029  relpeq1  44928  relpeq2  44929  relpeq3  44930  sprsymrelfolem2  47487  sprsymrelfo  47491  reuopreuprim  47520  dmatALTbasel  48397  lindslinindsimp2  48458  lmod1  48487  isnrm4  48925  iscnrm4  48948  isuplem  49174  isthinc  49414  thincciso  49448  thinccisod  49449