Theorem reuuni2 2941

Description: ∪{x ∈ A∣φ} is an explicit representation of "the unique element in A such that φ."

Hypothesis

Ref	Expression
reuuni2.1	⊢ (x = B → (φ ↔ ψ))

Assertion

Ref	Expression
reuuni2	⊢ ((B ∈ A ⋀ ∃!x ∈ A φ) → (ψ ↔ ∪{x ∈ A∣φ} = B))

Distinct variable groups:   x,A   x,B   ψ,x

Proof of Theorem reuuni2

Step	Hyp	Ref	Expression
1		ax-17 1012	. 2 ⊢ (y ∈ B → ∀x y ∈ B)
2		ax-17 1012	. . 3 ⊢ (ψ → ∀xψ)
3	2	a1i 8	. 2 ⊢ (B ∈ A → (ψ → ∀xψ))
4		reuuni2.1	. 2 ⊢ (x = B → (φ ↔ ψ))
5	1, 3, 4	reuuni2f 2940	1 ⊢ ((B ∈ A ⋀ ∃!x ∈ A φ) → (ψ ↔ ∪{x ∈ A∣φ} = B))

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230  ∀wal 995   = wceq 997   ∈ wcel 999  ∃!wreu 1694  {crab 1695  ∪cuni 2557

This theorem is referenced by:  reuuni3 2943  rabsnt 2951  f1ocnvfv3 3941  supub 4640  suplub 4641  suppr 4650  supsnALT 4652  lbinfm 6130  supxr 6163  flval2 6350  flbi 6352  uzinfmi 6488  isumclimtfi 7285  grpidinv2 8144  grpinv 8153  spwpr4OLD 8746  spwpr4aOLD 8747  pjeq2 9324  pjpj0i 9338  adjvalval 9944  cnlnadjlem5 10087  cnvbraval 10126  cdj3lem2 10446

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-reu 1698  df-rab 1699  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-uni 2558

Copyright terms: Public domain