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 3558. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2136. (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 3506 | . . . 4 ⊢ ∃𝑥 𝑥 = 𝐴 |
3 | vtocl.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | biimpd 230 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) |
5 | 2, 4 | eximii 1828 | . . 3 ⊢ ∃𝑥(𝜑 → 𝜓) |
6 | 5 | 19.36iv 1938 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) |
7 | vtocl.3 | . 2 ⊢ 𝜑 | |
8 | 6, 7 | mpg 1789 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 Vcvv 3492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 |
This theorem is referenced by: vtocl2 3559 vtocl3 3561 vtoclb 3562 zfauscl 5196 fnbrfvb 6711 caovcan 7341 uniex 7454 findcard2 8746 bnd2 9310 kmlem2 9565 axcc2lem 9846 dominf 9855 dcomex 9857 ac4c 9886 ac5 9887 dominfac 9983 pwfseqlem4 10072 grothomex 10239 ramub2 16338 ismred2 16862 utopsnneiplem 22783 dvfsumlem2 24551 plydivlem4 24812 bnj865 32094 bnj1015 32132 frmin 32981 poimirlem13 34786 poimirlem14 34787 poimirlem17 34790 poimirlem20 34793 poimirlem25 34798 poimirlem28 34801 poimirlem31 34804 poimirlem32 34805 voliunnfl 34817 volsupnfl 34818 prdsbnd2 34954 iscringd 35157 monotoddzzfi 39417 monotoddzz 39418 frege104 40191 dvgrat 40521 cvgdvgrat 40522 wessf1ornlem 41321 xrlexaddrp 41496 infleinf 41516 dvnmul 42104 dvnprodlem2 42108 fourierdlem41 42310 fourierdlem48 42316 fourierdlem49 42317 fourierdlem51 42319 fourierdlem71 42339 fourierdlem83 42351 fourierdlem97 42365 etransclem2 42398 etransclem46 42442 isomenndlem 42689 ovnsubaddlem1 42729 hoidmvlelem3 42756 vonicclem2 42843 smflimlem1 42924 smflimlem2 42925 smflimlem3 42926 funressndmafv2rn 43299 |
Copyright terms: Public domain | W3C validator |