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

Theorem elabd2 3670
Description: Membership in a class abstraction, using implicit substitution. Deduction version of elab 3681. (Contributed by GG, 12-Oct-2024.) (Revised by BJ, 16-Oct-2024.)
Hypotheses
Ref Expression
elabd2.ex (𝜑𝐴𝑉)
elabd2.eq (𝜑𝐵 = {𝑥𝜓})
elabd2.is ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
elabd2 (𝜑 → (𝐴𝐵𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜓(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem elabd2
StepHypRef Expression
1 elabd2.ex . 2 (𝜑𝐴𝑉)
2 elabd2.eq . . . . 5 (𝜑𝐵 = {𝑥𝜓})
32eleq2d 2825 . . . 4 (𝜑 → (𝐴𝐵𝐴 ∈ {𝑥𝜓}))
4 elab6g 3669 . . . 4 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜓} ↔ ∀𝑥(𝑥 = 𝐴𝜓)))
53, 4sylan9bb 509 . . 3 ((𝜑𝐴𝑉) → (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝜓)))
6 elisset 2821 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
7 elabd2.is . . . . . . . 8 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
87pm5.74da 804 . . . . . . 7 (𝜑 → ((𝑥 = 𝐴𝜓) ↔ (𝑥 = 𝐴𝜒)))
98albidv 1918 . . . . . 6 (𝜑 → (∀𝑥(𝑥 = 𝐴𝜓) ↔ ∀𝑥(𝑥 = 𝐴𝜒)))
10 19.23v 1940 . . . . . 6 (∀𝑥(𝑥 = 𝐴𝜒) ↔ (∃𝑥 𝑥 = 𝐴𝜒))
119, 10bitrdi 287 . . . . 5 (𝜑 → (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜒)))
12 pm5.5 361 . . . . 5 (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴𝜒) ↔ 𝜒))
1311, 12sylan9bb 509 . . . 4 ((𝜑 ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴𝜓) ↔ 𝜒))
146, 13sylan2 593 . . 3 ((𝜑𝐴𝑉) → (∀𝑥(𝑥 = 𝐴𝜓) ↔ 𝜒))
155, 14bitrd 279 . 2 ((𝜑𝐴𝑉) → (𝐴𝐵𝜒))
161, 15mpdan 687 1 (𝜑 → (𝐴𝐵𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535   = wceq 1537  wex 1776  wcel 2106  {cab 2712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814
This theorem is referenced by:  elabd3  3671  elimasng1  6107
  Copyright terms: Public domain W3C validator