![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-ceqsalt | Structured version Visualization version GIF version |
Description: Remove from ceqsalt 3504 dependency on ax-ext 2703 (and on df-cleq 2724 and df-v 3476). Note: this is not doable with ceqsralt 3505 (or ceqsralv 3512), which uses eleq1 2821, but the same dependence removal is possible for ceqsalg 3506, ceqsal 3508, ceqsalv 3510, cgsexg 3517, cgsex2g 3518, cgsex4g 3519, ceqsex 3521, ceqsexv 3523, ceqsex2 3527, ceqsex2v 3528, ceqsex3v 3529, ceqsex4v 3530, ceqsex6v 3531, ceqsex8v 3532, gencbvex 3533 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3534, gencbval 3535, vtoclgft 3538 (it uses Ⅎ, whose justification nfcjust 2884 does not use ax-ext 2703) and several other vtocl* theorems (see for instance bj-vtoclg1f 35666). See also bj-ceqsaltv 35635. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-ceqsalt | ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2815 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | 1 | 3anim3i 1154 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴)) |
3 | bj-ceqsalt0 35632 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1087 ∀wal 1539 = wceq 1541 ∃wex 1781 Ⅎwnf 1785 ∈ wcel 2106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-3an 1089 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-clel 2810 |
This theorem is referenced by: bj-ceqsalgALT 35638 |
Copyright terms: Public domain | W3C validator |