![]() |
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 2701 (and on df-cleq 2722 and df-v 3474). Note: this is not doable with ceqsralt 3505 (or ceqsralv 3512), which uses eleq1 2819, but the same dependence removal is possible for ceqsalg 3506, ceqsal 3508, ceqsalv 3510, cgsexg 3517, cgsex2g 3518, cgsex4g 3519, ceqsex 3522, ceqsexv 3524, ceqsex2 3528, ceqsex2v 3529, ceqsex3v 3530, ceqsex4v 3531, ceqsex6v 3532, ceqsex8v 3533, gencbvex 3534 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3535, gencbval 3536, vtoclgft 3539 (it uses Ⅎ, whose justification nfcjust 2882 does not use ax-ext 2701) and several other vtocl* theorems (see for instance bj-vtoclg1f 36101). See also bj-ceqsaltv 36070. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-ceqsalt | ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2813 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | 1 | 3anim3i 1152 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴)) |
3 | bj-ceqsalt0 36067 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ∃wex 1779 Ⅎwnf 1783 ∈ wcel 2104 |
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-12 2169 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1087 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-clel 2808 |
This theorem is referenced by: bj-ceqsalgALT 36073 |
Copyright terms: Public domain | W3C validator |