![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ceqsalv | Structured version Visualization version GIF version |
Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid ax-12 2170. (Revised by SN, 8-Sep-2024.) |
Ref | Expression |
---|---|
ceqsalv.1 | ⊢ 𝐴 ∈ V |
ceqsalv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ceqsalv | ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.23v 1944 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | |
2 | ceqsalv.2 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | pm5.74i 271 | . . 3 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) |
4 | 3 | albii 1820 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
5 | ceqsalv.1 | . . . 4 ⊢ 𝐴 ∈ V | |
6 | 5 | isseti 3489 | . . 3 ⊢ ∃𝑥 𝑥 = 𝐴 |
7 | 6 | a1bi 362 | . 2 ⊢ (𝜓 ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
8 | 1, 4, 7 | 3bitr4i 303 | 1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1538 = wceq 1540 ∃wex 1780 ∈ wcel 2105 Vcvv 3473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-clel 2809 |
This theorem is referenced by: ceqsexv 3525 ralxpxfr2d 3634 clel4OLD 3654 frsn 5763 raliunxp 5839 idrefALT 6112 funimass4 6956 fnssintima 7362 imaeqalov 7649 marypha2lem3 9435 kmlem12 10159 vdwmc2 16917 itg2leub 25485 eqscut2 27545 addsuniflem 27724 mulsuniflem 27844 nmoubi 30293 choc0 30847 nmopub 31429 nmfnleub 31446 elintfv 35041 heibor1lem 36981 elmapintrab 42630 |
Copyright terms: Public domain | W3C validator |