MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elimasng Structured version   Visualization version   GIF version

Theorem elimasng 5948
Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.)
Assertion
Ref Expression
elimasng ((𝐵𝑉𝐶𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))

Proof of Theorem elimasng
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 4569 . . . . 5 (𝑦 = 𝐵 → {𝑦} = {𝐵})
21imaeq2d 5922 . . . 4 (𝑦 = 𝐵 → (𝐴 “ {𝑦}) = (𝐴 “ {𝐵}))
32eleq2d 2896 . . 3 (𝑦 = 𝐵 → (𝑧 ∈ (𝐴 “ {𝑦}) ↔ 𝑧 ∈ (𝐴 “ {𝐵})))
4 opeq1 4795 . . . 4 (𝑦 = 𝐵 → ⟨𝑦, 𝑧⟩ = ⟨𝐵, 𝑧⟩)
54eleq1d 2895 . . 3 (𝑦 = 𝐵 → (⟨𝑦, 𝑧⟩ ∈ 𝐴 ↔ ⟨𝐵, 𝑧⟩ ∈ 𝐴))
63, 5bibi12d 348 . 2 (𝑦 = 𝐵 → ((𝑧 ∈ (𝐴 “ {𝑦}) ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐴) ↔ (𝑧 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝑧⟩ ∈ 𝐴)))
7 eleq1 2898 . . 3 (𝑧 = 𝐶 → (𝑧 ∈ (𝐴 “ {𝐵}) ↔ 𝐶 ∈ (𝐴 “ {𝐵})))
8 opeq2 4796 . . . 4 (𝑧 = 𝐶 → ⟨𝐵, 𝑧⟩ = ⟨𝐵, 𝐶⟩)
98eleq1d 2895 . . 3 (𝑧 = 𝐶 → (⟨𝐵, 𝑧⟩ ∈ 𝐴 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
107, 9bibi12d 348 . 2 (𝑧 = 𝐶 → ((𝑧 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝑧⟩ ∈ 𝐴) ↔ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)))
11 vex 3496 . . 3 𝑦 ∈ V
12 vex 3496 . . 3 𝑧 ∈ V
1311, 12elimasn 5947 . 2 (𝑧 ∈ (𝐴 “ {𝑦}) ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐴)
146, 10, 13vtocl2g 3570 1 ((𝐵𝑉𝐶𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1530  wcel 2107  {csn 4559  cop 4565  cima 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  elimasni  5949  eliniseg  5951  inimasn  6006  elpredim  6153  elpredg  6155  dffv3  6659  fvimacnv  6816  fvrnressn  6916  elecg  8324  imasnopn  22290  imasncld  22291  imasncls  22292  ustelimasn  22823  blval2  23164  elbl4  23165  1stpreimas  30433  opelco3  33011  scutval  33258  funpartfv  33399  eltail  33715  elecALTV  35519  brtrclfv2  40062  frege77d  40081  dfafv23  43442
  Copyright terms: Public domain W3C validator