Theorem hbab 1465

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

Hypothesis

Ref	Expression
hbab.1	⊢ (φ → ∀xφ)

Assertion

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

Distinct variable group:   x,z

Proof of Theorem hbab

Step	Hyp	Ref	Expression
1		ax-16 1208	. . 3 ⊢ (∀x x = z → ([z / y]φ → ∀x[z / y]φ))
2		hbab.1	. . . 4 ⊢ (φ → ∀xφ)
3	2	hbsb4 1246	. . 3 ⊢ (¬ ∀x x = z → ([z / y]φ → ∀x[z / y]φ))
4	1, 3	pm2.61i 126	. 2 ⊢ ([z / y]φ → ∀x[z / y]φ)
5		df-clab 1462	. 2 ⊢ (z ∈ {y∣φ} ↔ [z / y]φ)
6	5	albii 997	. 2 ⊢ (∀x z ∈ {y∣φ} ↔ ∀x[z / y]φ)
7	4, 5, 6	3imtr4 219	1 ⊢ (z ∈ {y∣φ} → ∀x z ∈ {y∣φ})

Syntax hints:   → wi 3  ∀wal 952   = wceq 954   ∈ wcel 956  [wsbc 1168  {cab 1461

This theorem is referenced by:  hbrab 1770  cbvab 1904  hbeqd 1909  hbeld 1910  hbsbc1gd 1979  hbsbcgd 1980  hbif 2369  hbopd 2494  intab 2556  hbiu1 2580  hbii1 2581  hbbrd 2655  moop2 2798  hbopab1 2810  hbopab2 2811  hbimad 3410  hbfv 3731  hbfvd 3732  hbfvd2 3733  fvopabgf 3789  fvopabnf 3790  hbrdg 3938  hboprd 3984  hboprab1 3995  hboprab2 3996  oprabval4g 4033  hta 4720  hbnegd 5355  seq1lem1 6266  hbsum1 6941  hbsum 6942  fsum1f 6965  fsump1f 6969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462

Copyright terms: Public domain