|   | 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 2140. (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 233 | . 2 ⊢ (𝑥 = 𝐴 → 𝜓) | 
| 5 | 1, 4 | vtocle 3554 | 1 ⊢ 𝜓 | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 ∈ wcel 2107 Vcvv 3479 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-clel 2815 | 
| This theorem is referenced by: vtocl2 3565 vtocl3 3566 vtoclb 3567 zfauscl 5297 fnbrfvb 6958 caovcan 7638 findcard2 9205 bnd2 9934 kmlem2 10193 axcc2lem 10477 dominf 10486 dcomex 10488 ac4c 10517 ac5 10518 dominfac 10614 grothomex 10870 ramub2 17053 ismred2 17647 utopsnneiplem 24257 dvfsumlem2 26068 dvfsumlem2OLD 26069 plydivlem4 26339 bnj865 34938 bnj1015 34977 poimirlem13 37641 poimirlem14 37642 poimirlem17 37645 poimirlem20 37648 poimirlem25 37653 poimirlem28 37656 poimirlem31 37659 poimirlem32 37660 voliunnfl 37672 volsupnfl 37673 prdsbnd2 37803 iscringd 38006 monotoddzzfi 42959 monotoddzz 42960 frege104 43985 dvgrat 44336 cvgdvgrat 44337 wessf1ornlem 45195 xrlexaddrp 45368 infleinf 45388 dvnmul 45963 dvnprodlem2 45967 fourierdlem41 46168 fourierdlem48 46174 fourierdlem49 46175 fourierdlem51 46177 fourierdlem71 46197 fourierdlem83 46209 fourierdlem97 46223 etransclem2 46256 etransclem46 46300 isomenndlem 46550 ovnsubaddlem1 46590 hoidmvlelem3 46617 vonicclem2 46704 smflimlem1 46791 smflimlem2 46792 smflimlem3 46793 funressndmafv2rn 47240 | 
| Copyright terms: Public domain | W3C validator |