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 3475. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2141. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) |
Ref | Expression |
---|---|
vtocl.1 | ⊢ 𝐴 ∈ V |
vtocl.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtocl.3 | . . 3 ⊢ 𝜑 | |
2 | vtocl.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | mpbii 236 | . 2 ⊢ (𝑥 = 𝐴 → 𝜓) |
4 | vtocl.1 | . . 3 ⊢ 𝐴 ∈ V | |
5 | 4 | isseti 3423 | . 2 ⊢ ∃𝑥 𝑥 = 𝐴 |
6 | 3, 5 | exlimiiv 1939 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 ∈ wcel 2110 Vcvv 3408 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-clel 2816 |
This theorem is referenced by: vtocl2 3476 vtocl3 3477 vtoclb 3478 zfauscl 5194 fnbrfvb 6765 caovcan 7412 findcard2 8842 findcard2OLD 8913 frmin 9365 bnd2 9509 kmlem2 9765 axcc2lem 10050 dominf 10059 dcomex 10061 ac4c 10090 ac5 10091 dominfac 10187 pwfseqlem4 10276 grothomex 10443 ramub2 16567 ismred2 17106 utopsnneiplem 23145 dvfsumlem2 24924 plydivlem4 25189 bnj865 32616 bnj1015 32655 poimirlem13 35527 poimirlem14 35528 poimirlem17 35531 poimirlem20 35534 poimirlem25 35539 poimirlem28 35542 poimirlem31 35545 poimirlem32 35546 voliunnfl 35558 volsupnfl 35559 prdsbnd2 35690 iscringd 35893 monotoddzzfi 40467 monotoddzz 40468 frege104 41252 dvgrat 41603 cvgdvgrat 41604 wessf1ornlem 42395 xrlexaddrp 42564 infleinf 42584 dvnmul 43159 dvnprodlem2 43163 fourierdlem41 43364 fourierdlem48 43370 fourierdlem49 43371 fourierdlem51 43373 fourierdlem71 43393 fourierdlem83 43405 fourierdlem97 43419 etransclem2 43452 etransclem46 43496 isomenndlem 43743 ovnsubaddlem1 43783 hoidmvlelem3 43810 vonicclem2 43897 smflimlem1 43978 smflimlem2 43979 smflimlem3 43980 funressndmafv2rn 44387 |
Copyright terms: Public domain | W3C validator |