Theorem hbab 1096

Description: A variable not free in a wff remains so in an class abstraction.

Hypothesis

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

Assertion

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

Distinct variable group(s):   x,z

Proof of Theorem hbab

Step	Hyp	Ref	Expression
1		ax-16 922	. . 3 ⊢ (∀x x = z → ([z / y]φ → ∀x[z / y]φ))
2		hbab.1	. . . 4 ⊢ (φ → ∀xφ)
3	2	hbsb4 905	. . 3 ⊢ (¬ ∀x x = z → ([z / y]φ → ∀x[z / y]φ))
4	1, 3	pm2.61i 110	. 2 ⊢ ([z / y]φ → ∀x[z / y]φ)
5		df-clab 1093	. 2 ⊢ (z ∈ {y∣φ} ↔ [z / y]φ)
6	5	bial 695	. 2 ⊢ (∀x z ∈ {y∣φ} ↔ ∀x[z / y]φ)
7	4, 5, 6	3imtr4 192	1 ⊢ (z ∈ {y∣φ} → ∀x z ∈ {y∣φ})

Syntax hints:   → wi 2  ∀wal 672   = weq 797  [wsb 852  {cab 1090   ∈ wcel 1092

This theorem is referenced by:  hbrab 1311  cbvab 1423  moop2 1910  hbiu1 2012  hbii1 2013  hbopab1 2112  hbopab2 2113  hbfv 2837  fvopabgf 2874  fvopabnf 2875  hbrdg 2974  hboprab1 3023  hboprab2 3024  oprabval4g 3053  hta 3619  seqlem1 4662

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093

metamath.org