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.) |
Ref | Expression |
---|---|
ceqsalv.1 | ⊢ 𝐴 ∈ V |
ceqsalv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ceqsalv | ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ceqsalv.1 | . 2 ⊢ 𝐴 ∈ V | |
3 | ceqsalv.2 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | ceqsal 3205 | 1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 = wceq 1475 ∈ wcel 1977 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 |
This theorem is referenced by: ralxpxfr2d 3298 clel2 3309 clel4 3312 frsn 5112 raliunxp 5183 fv3 6116 funimass4 6157 marypha2lem3 8226 kmlem12 8866 fpwwe2lem12 9342 vdwmc2 15521 itg2leub 23307 nmoubi 27011 choc0 27569 nmopub 28151 nmfnleub 28168 heibor1lem 32778 elmapintrab 36901 |
Copyright terms: Public domain | W3C validator |