Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem hbra1 1679

Description: is not free in .

Assertion

Ref	Expression
hbra1

---

Proof of Theorem hbra1

Step	Hyp	Ref	Expression
1		hba1 1000	. 2
2		df-ral 1641	. 2
3	2	albii 996	. 2
4	1, 2, 3	3imtr4 219	1

Colors of variables: wff set class

Syntax hints:   wi 3  wal 951   wcel 955  wral 1637

This theorem is referenced by:  r19.12 1732  r19.15 1745  uniiunlem 2122  ralidm 2347  ss2iun 2567  iineq2 2569  hbii1 2575  dfiun2g 2576  ralxfrd 2887  ralxfr 2889  peano5 3143  tfinds 3151  ralxp 3208  zfrep6 3600  fnopabg 3601  elrnopabg 3785  chfnrn 3787  fopab2 3808  ffnfv 3813  isotrALT 3883  iunon 3894  iinon 3895  tfrlem1 3896  tfr3 3911  tz7.48-1 3941  tz7.49 3944  elrnoprabg 4108  nneneq 4492  r1tr 4626  scottex 4688  aceq6b 4714  zorn2lem5 4764  lble 5994  bccl2t 6909  sumeq2 6923  clm4le 7019  clm0 7021  clm0nns 7023  climsup 7091  caucvglem6 7098  rnbra 9953  irredt 10230  cmphmp 10408  homcard 10426  imonclem 10583  ismonc 10584  cmpmon 10585

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641

Copyright terms: Public domain