Theorem abbi2dv 1575

Description: Deduction from a wff to a class abstraction.

Hypothesis

Ref	Expression
abbirdv.1	⊢ (φ → (x ∈ A ↔ ψ))

Assertion

Ref	Expression
abbi2dv	⊢ (φ → A = {x∣ψ})

Distinct variable groups:   x,A   φ,x

Proof of Theorem abbi2dv

Step	Hyp	Ref	Expression
1		abbirdv.1	. . 3 ⊢ (φ → (x ∈ A ↔ ψ))
2	1	19.21aiv 1284	. 2 ⊢ (φ → ∀x(x ∈ A ↔ ψ))
3		abeq2 1565	. 2 ⊢ (A = {x∣ψ} ↔ ∀x(x ∈ A ↔ ψ))
4	2, 3	sylibr 200	1 ⊢ (φ → A = {x∣ψ})

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 952   = wceq 954   ∈ wcel 956  {cab 1461

This theorem is referenced by:  sbab 1580  rabbirdv 2217  iftrue 2362  iffalse 2363  iin0 2735  iniseg 3422  isoini 3891  pw2en 4432  r1val2 4658  aceq3 4713  tgval3t 7575  metnei 7830  grpinvf 8029

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-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

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

Copyright terms: Public domain