![]() |
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. See also vtoclALT 3473. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2077. (Revised by BJ, 29-Nov-2020.) |
Ref | Expression |
---|---|
vtocl.1 | ⊢ 𝐴 ∈ V |
vtocl.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtocl.1 | . . . . 5 ⊢ 𝐴 ∈ V | |
2 | 1 | isseti 3423 | . . . 4 ⊢ ∃𝑥 𝑥 = 𝐴 |
3 | vtocl.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | biimpd 221 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) |
5 | 2, 4 | eximii 1799 | . . 3 ⊢ ∃𝑥(𝜑 → 𝜓) |
6 | 5 | 19.36iv 1905 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) |
7 | vtocl.3 | . 2 ⊢ 𝜑 | |
8 | 6, 7 | mpg 1760 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1507 ∈ wcel 2048 Vcvv 3409 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 df-clel 2840 |
This theorem is referenced by: vtocl2 3474 vtocl3 3476 vtoclb 3477 zfauscl 5056 fnbrfvb 6542 caovcan 7162 uniex 7277 findcard2 8545 bnd2 9108 kmlem2 9363 axcc2lem 9648 dominf 9657 dcomex 9659 ac4c 9688 ac5 9689 dominfac 9785 pwfseqlem4 9874 grothomex 10041 ramub2 16196 ismred2 16722 utopsnneiplem 22549 dvfsumlem2 24317 plydivlem4 24578 bnj865 31803 bnj1015 31841 frmin 32545 poimirlem13 34294 poimirlem14 34295 poimirlem17 34298 poimirlem20 34301 poimirlem25 34306 poimirlem28 34309 poimirlem31 34312 poimirlem32 34313 voliunnfl 34325 volsupnfl 34326 prdsbnd2 34463 iscringd 34666 monotoddzzfi 38880 monotoddzz 38881 frege104 39621 dvgrat 40004 cvgdvgrat 40005 wessf1ornlem 40815 xrlexaddrp 40995 infleinf 41015 dvnmul 41604 dvnprodlem2 41608 fourierdlem41 41810 fourierdlem48 41816 fourierdlem49 41817 fourierdlem51 41819 fourierdlem71 41839 fourierdlem83 41851 fourierdlem97 41865 etransclem2 41898 etransclem46 41942 isomenndlem 42189 ovnsubaddlem1 42229 hoidmvlelem3 42256 vonicclem2 42343 smflimlem1 42424 smflimlem2 42425 smflimlem3 42426 funressndmafv2rn 42774 |
Copyright terms: Public domain | W3C validator |