Theorem hbra1 2147

Description: x is not free in A.x e. Aph.

Assertion

Ref	Expression
hbra1	|- (A.x e. A ph -> A.xA.x e. A ph)

Proof of Theorem hbra1

Step	Hyp	Ref	Expression
1		hba1 1350	. 2 |- (A.x(x e. A -> ph) -> A.xA.x(x e. A -> ph))
2		df-ral 2109	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
3	2	albii 1346	. 2 |- (A.xA.x e. A ph <-> A.xA.x(x e. A -> ph))
4	1, 2, 3	3imtr4i 236	1 |- (A.x e. A ph -> A.xA.x e. A ph)

Syntax hints:   -> wi 3  A.wal 1296   e. wcel 1300  A.wral 2105

This theorem is referenced by:  r19.12 2204  r19.12OLD 2205  ralbi 2223  ssralv2 2674  uniiunlem 2693  ralidm 2973  ss2iunOLD 3272  iineq2OLD 3275  hbii1 3282  dfiun2g 3283  dfiun2gOLD 3284  eufromeq1 3828  eufromeq2 3829  eufromeq5 3832  eufromeq6 3833  euobj1 3834  ralxfrd 3837  ralxfr 3839  tfinds 3942  tfindsOLD 3943  peano5 3975  ralxp 4041  asymref2 4310  zfrep6 4545  fnopabg 4546  elrnopabg 4773  chfnrn 4775  fopab2 4796  ffnfv 4801  isotrALT 4875  elrnoprabg 5066  iunon 5114  iinon 5115  onopriun 5118  tfrlem1 5119  tfr3 5134  tz7.48-1 5165  tz7.49 5168  ac6sfilem3 5508  nneneq 5606  ordtypelem6 5689  ordtypelem7 5690  r1tr 5765  tratrb 5831  scottex 5846  omsubsdomlem2 5880  elomsubsd 5885  aceq6b 5904  zorn2lem5 5954  lble 7256  bccl2 8223  sumeq2 8245  clm4lei 8341  clm0i 8343  clm0nnsi 8345  climabs0i 8373  climsupi 8415  caucvglem6 8422  metequiv 9158  gafo 9451  indexfi 10174  rnbra 11678  irred 11967  bnj10 12374  bnj1095 12915  bnj1218 12992  bnj1347 13080  bnj1379 13100  bnj1229 13457  bnj1268 13472  bnj1309 13487  bnj1307 13488  bnj1388 13514  bnj1398 13515  bnj1444 13534  bnj1487 13552  bnj1499 13561  bnj1505 13564  bnj1525 13572  r19.21 13818  dfon2lem3 13851  wfrlem4 13960  imgfldref2 14368  fopab2g 14485  hbcp 14500  dutos1 14626  tostos 14637  prodeq2 14661  fnopabco2b 14734  curgrpact 14735  fprodneg 14741  cmphmp 14878  homcard 14893  bwt2 14960  imonclem 15162  ismonc 15163  cmpmon 15164  iepiclem 15172  isepic 15173  taralt 15211  ordtypelem6OLD 15380  ordtypelem7OLD 15381  omsubsdomlem2OLD 15389  elomsubsdOLD 15394  hscptsscld 15434  alexsublem3 15439  neibastop1 15518  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  limfilcf 15587  cover2 15673  hbixp1 15725  indexdom 15754  indexfiOLD 15755  filbcmb 15776  fsumleisumi 15826  mettrifi 15847  totbndbnd 15944  smores 16446  hbra2VD 16684  tratrbVD 16685  ssralv2VD 16690  glbconx 17029  pmapglbx 17251  pmapglb2x 17254

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain