Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-elgab Structured version   Visualization version   GIF version

Theorem bj-elgab 35135
Description: Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.)
Hypotheses
Ref Expression
bj-elgab.nf (𝜑 → ∀𝑥𝜑)
bj-elgab.nfa (𝜑𝑥𝐴)
bj-elgab.ex (𝜑𝐴𝑉)
bj-elgab.is (𝜑 → (∃𝑥(𝐴 = 𝐵𝜓) ↔ 𝜒))
Assertion
Ref Expression
bj-elgab (𝜑 → (𝐴 ∈ {𝐵𝑥𝜓} ↔ 𝜒))

Proof of Theorem bj-elgab
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-bj-gab 35130 . . 3 {𝐵𝑥𝜓} = {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)}
21eleq2i 2830 . 2 (𝐴 ∈ {𝐵𝑥𝜓} ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)})
3 bj-elgab.ex . . . 4 (𝜑𝐴𝑉)
4 bj-elgab.nf . . . . . . . . 9 (𝜑 → ∀𝑥𝜑)
54adantr 481 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → ∀𝑥𝜑)
6 bj-elgab.nfa . . . . . . . . . 10 (𝜑𝑥𝐴)
7 nfcvd 2908 . . . . . . . . . . . 12 (𝑥𝐴𝑥𝑦)
8 id 22 . . . . . . . . . . . 12 (𝑥𝐴𝑥𝐴)
97, 8nfeqd 2917 . . . . . . . . . . 11 (𝑥𝐴 → Ⅎ𝑥 𝑦 = 𝐴)
109nf5rd 2189 . . . . . . . . . 10 (𝑥𝐴 → (𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴))
116, 10syl 17 . . . . . . . . 9 (𝜑 → (𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴))
1211imp 407 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → ∀𝑥 𝑦 = 𝐴)
13 19.26 1873 . . . . . . . 8 (∀𝑥(𝜑𝑦 = 𝐴) ↔ (∀𝑥𝜑 ∧ ∀𝑥 𝑦 = 𝐴))
145, 12, 13sylanbrc 583 . . . . . . 7 ((𝜑𝑦 = 𝐴) → ∀𝑥(𝜑𝑦 = 𝐴))
15 eqeq2 2750 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝐵 = 𝑦𝐵 = 𝐴))
16 eqcom 2745 . . . . . . . . . 10 (𝐵 = 𝐴𝐴 = 𝐵)
1715, 16bitrdi 287 . . . . . . . . 9 (𝑦 = 𝐴 → (𝐵 = 𝑦𝐴 = 𝐵))
1817anbi1d 630 . . . . . . . 8 (𝑦 = 𝐴 → ((𝐵 = 𝑦𝜓) ↔ (𝐴 = 𝐵𝜓)))
1918adantl 482 . . . . . . 7 ((𝜑𝑦 = 𝐴) → ((𝐵 = 𝑦𝜓) ↔ (𝐴 = 𝐵𝜓)))
2014, 19exbidh 1870 . . . . . 6 ((𝜑𝑦 = 𝐴) → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓)))
2120ex 413 . . . . 5 (𝜑 → (𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓))))
2221alrimiv 1930 . . . 4 (𝜑 → ∀𝑦(𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓))))
23 elabgt 3602 . . . 4 ((𝐴𝑉 ∧ ∀𝑦(𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓)))) → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ ∃𝑥(𝐴 = 𝐵𝜓)))
243, 22, 23syl2anc 584 . . 3 (𝜑 → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ ∃𝑥(𝐴 = 𝐵𝜓)))
25 bj-elgab.is . . 3 (𝜑 → (∃𝑥(𝐴 = 𝐵𝜓) ↔ 𝜒))
2624, 25bitrd 278 . 2 (𝜑 → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ 𝜒))
272, 26syl5bb 283 1 (𝜑 → (𝐴 ∈ {𝐵𝑥𝜓} ↔ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1537   = wceq 1539  wex 1782  wcel 2106  {cab 2715  wnfc 2887  {bj-cgab 35129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-bj-gab 35130
This theorem is referenced by:  bj-gabima  35136
  Copyright terms: Public domain W3C validator