![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtocl | Structured version Visualization version GIF version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2130. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 20-Jun-2025.) |
Ref | Expression |
---|---|
vtocl.1 | ⊢ 𝐴 ∈ V |
vtocl.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtocl.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | vtocl.3 | . . 3 ⊢ 𝜑 | |
3 | vtocl.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | mpbii 232 | . 2 ⊢ (𝑥 = 𝐴 → 𝜓) |
5 | 1, 4 | vtocle 3535 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 Vcvv 3462 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-clel 2803 |
This theorem is referenced by: vtocl2 3547 vtocl3 3548 vtoclb 3549 zfauscl 5306 fnbrfvb 6954 caovcan 7630 findcard2 9202 findcard2OLD 9318 bnd2 9936 kmlem2 10194 axcc2lem 10479 dominf 10488 dcomex 10490 ac4c 10519 ac5 10520 dominfac 10616 pwfseqlem4 10705 grothomex 10872 ramub2 17016 ismred2 17616 utopsnneiplem 24243 dvfsumlem2 26052 dvfsumlem2OLD 26053 plydivlem4 26324 bnj865 34768 bnj1015 34807 poimirlem13 37334 poimirlem14 37335 poimirlem17 37338 poimirlem20 37341 poimirlem25 37346 poimirlem28 37349 poimirlem31 37352 poimirlem32 37353 voliunnfl 37365 volsupnfl 37366 prdsbnd2 37496 iscringd 37699 monotoddzzfi 42600 monotoddzz 42601 frege104 43634 dvgrat 43986 cvgdvgrat 43987 wessf1ornlem 44792 xrlexaddrp 44967 infleinf 44987 dvnmul 45564 dvnprodlem2 45568 fourierdlem41 45769 fourierdlem48 45775 fourierdlem49 45776 fourierdlem51 45778 fourierdlem71 45798 fourierdlem83 45810 fourierdlem97 45824 etransclem2 45857 etransclem46 45901 isomenndlem 46151 ovnsubaddlem1 46191 hoidmvlelem3 46218 vonicclem2 46305 smflimlem1 46392 smflimlem2 46393 smflimlem3 46394 funressndmafv2rn 46836 |
Copyright terms: Public domain | W3C validator |