Theorem hbab1 1465

Description: Bound-variable hypothesis builder for a class abstraction.

Assertion

Ref	Expression
hbab1	⊢ (y ∈ {x∣φ} → ∀x y ∈ {x∣φ})

Distinct variable group:   x,y

Proof of Theorem hbab1

Step	Hyp	Ref	Expression
1		hbs1 1331	. 2 ⊢ ([y / x]φ → ∀x[y / x]φ)
2		df-clab 1463	. 2 ⊢ (y ∈ {x∣φ} ↔ [y / x]φ)
3	2	albii 998	. 2 ⊢ (∀x y ∈ {x∣φ} ↔ ∀x[y / x]φ)
4	1, 2, 3	3imtr4 219	1 ⊢ (y ∈ {x∣φ} → ∀x y ∈ {x∣φ})

Syntax hints:   → wi 3  ∀wal 953   ∈ wcel 957  [wsbc 1169  {cab 1462

This theorem is referenced by:  abeq2 1566  eq2ab 1571  hbrab1 1770  elabgt 1892  elabf 1893  elabgf 1895  cbvab 1905  ss2ab 2113  abn0 2287  eusn 2443  eluniab 2509  elintab 2540  ssintab 2546  zfrep4 2697  euuni 2877  reucl 2881  onminex 3016  iunon 3904  iinon 3905  iunfi 4552  scott0 4700  scottexs 4701  scott0s 4702  cp 4705  hta 4711  cardprc 4844  tgval3t 7585

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-10 965  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463

Copyright terms: Public domain