![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtocl2g | Structured version Visualization version GIF version |
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2138, ax-11 2155, and ax-13 2372. (Revised by Steven Nguyen, 29-Nov-2022.) |
Ref | Expression |
---|---|
vtocl2g.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl2g.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
vtocl2g.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl2g | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3493 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | vtocl2g.2 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
3 | 2 | imbi2d 341 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒))) |
4 | vtocl2g.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | vtocl2g.3 | . . . 4 ⊢ 𝜑 | |
6 | 4, 5 | vtoclg 3557 | . . 3 ⊢ (𝐴 ∈ V → 𝜓) |
7 | 3, 6 | vtoclg 3557 | . 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒)) |
8 | 1, 7 | mpan9 508 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 Vcvv 3475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 |
This theorem is referenced by: vtocl3g 3564 vtocl4g 3572 uniprgOLD 4929 intprgOLD 4989 opthg 5478 opelopabsb 5531 vtoclr 5740 elimasngOLD 6090 funopg 6583 f1osng 6875 fsng 7135 fnpr2g 7212 unexb 7735 op1stg 7987 op2ndg 7988 xpsneng 9056 xpcomeng 9064 sbth 9093 sbthfi 9202 unxpdom 9253 fpwwe2lem4 10629 prcdnq 10988 mhmlem 18945 carsgmon 33344 brimageg 34930 brdomaing 34938 brrangeg 34939 rankung 35169 mbfresfi 36582 zindbi 41733 2sbc6g 43222 2sbc5g 43223 fmulcl 44345 |
Copyright terms: Public domain | W3C validator |