Theorem hbra1 1733

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 1039	. 2 |- (A.x(x e. A -> ph) -> A.xA.x(x e. A -> ph))
2		df-ral 1695	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
3	2	albii 1035	. 2 |- (A.xA.x e. A ph <-> A.xA.x(x e. A -> ph))
4	1, 2, 3	3imtr4i 217	1 |- (A.x e. A ph -> A.xA.x e. A ph)

Syntax hints:   -> wi 3  A.wal 990   e. wcel 994  A.wral 1691

This theorem is referenced by:  r19.12 1786  r19.15 1799  uniiunlem 2184  ralidm 2411  ss2iun 2645  iineq2 2647  hbii1 2653  dfiun2g 2654  ralxfrd 3120  ralxfr 3122  tfinds 3212  peano5 3241  ralxp 3301  zfrep6 3721  fnopabg 3722  elrnopabg 3914  chfnrn 3916  fopab2 3937  ffnfv 3942  isotrALT 4012  elrnoprabg 4186  iunon 4207  iinon 4208  onopriun 4211  tfrlem1 4212  tfr3 4227  tz7.48-1 4257  tz7.49 4260  ac6sfilem3 4590  nneneq 4659  r1tr 4800  scottex 4862  aceq6b 4888  zorn2lem5 4938  lble 6215  bccl2 7174  sumeq2 7188  clm4lei 7284  clm0i 7286  clm0nnsi 7288  climabs0i 7316  climsupi 7358  caucvglem6 7365  metequiv 8091  rnbra 10320  irred 10604  imgfldref2 10768  tostos 10883  cmphmp 11027  homcard 11045  bwt2 11123  imonclem 11268  ismonc 11269  cmpmon 11270  iepiclem 11278  isepic 11279  ordtypelem6 11432  ordtypelem7 11433  omsubsdomlem2 11441  elomsubsd 11446  hscptsscld 11491  alexsublem3 11498  topbasfne 11560  neibastop1 11579  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  limfilcf 11683  gafo 11773  indexd 11846  indexf 11847  filbcmb 11857  fsumleisumi 11889  mettrifi 11912  totbndbnd 12000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223  df-ral 1695

Copyright terms: Public domain