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 36122
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 36117 . . 3 {𝐵𝑥𝜓} = {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)}
21eleq2i 2823 . 2 (𝐴 ∈ {𝐵𝑥𝜓} ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)})
3 bj-elgab.ex . . . 4 (𝜑𝐴𝑉)
4 bj-elgab.nf . . . . . . . . 9 (𝜑 → ∀𝑥𝜑)
54adantr 479 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → ∀𝑥𝜑)
6 bj-elgab.nfa . . . . . . . . . 10 (𝜑𝑥𝐴)
7 nfcvd 2902 . . . . . . . . . . . 12 (𝑥𝐴𝑥𝑦)
8 id 22 . . . . . . . . . . . 12 (𝑥𝐴𝑥𝐴)
97, 8nfeqd 2911 . . . . . . . . . . 11 (𝑥𝐴 → Ⅎ𝑥 𝑦 = 𝐴)
109nf5rd 2187 . . . . . . . . . 10 (𝑥𝐴 → (𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴))
116, 10syl 17 . . . . . . . . 9 (𝜑 → (𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴))
1211imp 405 . . . . . . . 8 ((𝜑𝑦 = 𝐴) → ∀𝑥 𝑦 = 𝐴)
13 19.26 1871 . . . . . . . 8 (∀𝑥(𝜑𝑦 = 𝐴) ↔ (∀𝑥𝜑 ∧ ∀𝑥 𝑦 = 𝐴))
145, 12, 13sylanbrc 581 . . . . . . 7 ((𝜑𝑦 = 𝐴) → ∀𝑥(𝜑𝑦 = 𝐴))
15 eqeq2 2742 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝐵 = 𝑦𝐵 = 𝐴))
16 eqcom 2737 . . . . . . . . . 10 (𝐵 = 𝐴𝐴 = 𝐵)
1715, 16bitrdi 286 . . . . . . . . 9 (𝑦 = 𝐴 → (𝐵 = 𝑦𝐴 = 𝐵))
1817anbi1d 628 . . . . . . . 8 (𝑦 = 𝐴 → ((𝐵 = 𝑦𝜓) ↔ (𝐴 = 𝐵𝜓)))
1918adantl 480 . . . . . . 7 ((𝜑𝑦 = 𝐴) → ((𝐵 = 𝑦𝜓) ↔ (𝐴 = 𝐵𝜓)))
2014, 19exbidh 1868 . . . . . 6 ((𝜑𝑦 = 𝐴) → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓)))
2120ex 411 . . . . 5 (𝜑 → (𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓))))
2221alrimiv 1928 . . . 4 (𝜑 → ∀𝑦(𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓))))
23 elabgt 3661 . . . 4 ((𝐴𝑉 ∧ ∀𝑦(𝑦 = 𝐴 → (∃𝑥(𝐵 = 𝑦𝜓) ↔ ∃𝑥(𝐴 = 𝐵𝜓)))) → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ ∃𝑥(𝐴 = 𝐵𝜓)))
243, 22, 23syl2anc 582 . . 3 (𝜑 → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ ∃𝑥(𝐴 = 𝐵𝜓)))
25 bj-elgab.is . . 3 (𝜑 → (∃𝑥(𝐴 = 𝐵𝜓) ↔ 𝜒))
2624, 25bitrd 278 . 2 (𝜑 → (𝐴 ∈ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ 𝜒))
272, 26bitrid 282 1 (𝜑 → (𝐴 ∈ {𝐵𝑥𝜓} ↔ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1537   = wceq 1539  wex 1779  wcel 2104  {cab 2707  wnfc 2881  {bj-cgab 36116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-bj-gab 36117
This theorem is referenced by:  bj-gabima  36123
  Copyright terms: Public domain W3C validator