![]() |
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 3514 dependency on ax-ext 2707 (and on df-cleq 2728 and df-v 3481). Note: this is not doable with ceqsralt 3515 (or ceqsralv 3521), which uses eleq1 2828, but the same dependence removal is possible for ceqsalg 3516, ceqsal 3518, ceqsalv 3520, cgsexg 3525, cgsex2g 3526, cgsex4g 3527, ceqsex 3529, ceqsexv 3531, ceqsex2 3534, ceqsex2v 3535, ceqsex3v 3536, ceqsex4v 3537, ceqsex6v 3538, ceqsex8v 3539, gencbvex 3540 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3541, gencbval 3542, vtoclgft 3551 (it uses Ⅎ, whose justification nfcjust 2890 does not use ax-ext 2707) and several other vtocl* theorems (see for instance bj-vtoclg1f 36897). See also bj-ceqsaltv 36866. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-ceqsalt | ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2822 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | 1 | 3anim3i 1155 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴)) |
3 | bj-ceqsalt0 36863 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1087 ∀wal 1538 = wceq 1540 ∃wex 1779 Ⅎwnf 1783 ∈ wcel 2108 |
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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-12 2177 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2714 df-clel 2815 |
This theorem is referenced by: bj-ceqsalgALT 36869 |
Copyright terms: Public domain | W3C validator |