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 3438 dependency on ax-ext 2708 (and on df-cleq 2729 and df-v 3410). Note: this is not doable with ceqsralt 3439 (or ceqsralv 3445), which uses eleq1 2825, but the same dependence removal is possible for ceqsalg 3440, ceqsal 3442, ceqsalv 3443, cgsexg 3450, cgsex2g 3451, cgsex4g 3452, ceqsex 3454, ceqsexv 3455, ceqsex2 3458, ceqsex2v 3459, ceqsex3v 3460, ceqsex4v 3461, ceqsex6v 3462, ceqsex8v 3463, gencbvex 3464 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3465, gencbval 3466, vtoclgft 3468 (it uses Ⅎ, whose justification nfcjust 2885 does not use ax-ext 2708) and several other vtocl* theorems (see for instance bj-vtoclg1f 34840). See also bj-ceqsaltv 34809. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-ceqsalt | ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-elisset 34798 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | 1 | 3anim3i 1156 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴)) |
3 | bj-ceqsalt0 34806 | . 2 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥 𝑥 = 𝐴) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | |
4 | 2, 3 | syl 17 | 1 ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ w3a 1089 ∀wal 1541 = wceq 1543 ∃wex 1787 Ⅎwnf 1791 ∈ wcel 2110 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1091 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-clel 2816 |
This theorem is referenced by: bj-ceqsalgALT 34812 |
Copyright terms: Public domain | W3C validator |