![]() |
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 2172. (Revised by SN, 8-Sep-2024.) |
Ref | Expression |
---|---|
ceqsalv.1 | ⊢ 𝐴 ∈ V |
ceqsalv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ceqsalv | ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.23v 1946 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | |
2 | ceqsalv.2 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | pm5.74i 271 | . . 3 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) |
4 | 3 | albii 1822 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
5 | ceqsalv.1 | . . . 4 ⊢ 𝐴 ∈ V | |
6 | 5 | isseti 3459 | . . 3 ⊢ ∃𝑥 𝑥 = 𝐴 |
7 | 6 | a1bi 363 | . 2 ⊢ (𝜓 ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
8 | 1, 4, 7 | 3bitr4i 303 | 1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 = wceq 1542 ∃wex 1782 ∈ wcel 2107 Vcvv 3444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-clel 2816 |
This theorem is referenced by: ceqsexv 3493 ralxpxfr2d 3595 clel4OLD 3615 frsn 5718 raliunxp 5794 idrefALT 6064 funimass4 6905 fnssintima 7304 marypha2lem3 9332 kmlem12 10056 vdwmc2 16811 itg2leub 25051 eqscut2 27097 nmoubi 29543 choc0 30097 nmopub 30679 nmfnleub 30696 imaeqalov 34108 elintfv 34149 addsunif 34301 heibor1lem 36200 elmapintrab 41753 |
Copyright terms: Public domain | W3C validator |