![]() |
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 2137, ax-11 2154, and ax-13 2370. (Revised by Steven Nguyen, 29-Nov-2022.) |
Ref | Expression |
---|---|
vtocl2g.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl2g.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
vtocl2g.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl2g | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3491 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | vtocl2g.2 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
3 | 2 | imbi2d 340 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒))) |
4 | vtocl2g.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | vtocl2g.3 | . . . 4 ⊢ 𝜑 | |
6 | 4, 5 | vtoclg 3553 | . . 3 ⊢ (𝐴 ∈ V → 𝜓) |
7 | 3, 6 | vtoclg 3553 | . 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒)) |
8 | 1, 7 | mpan9 507 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 Vcvv 3473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 |
This theorem is referenced by: vtocl3g 3560 vtocl4g 3568 uniprgOLD 4921 intprgOLD 4981 opthg 5470 opelopabsb 5523 vtoclr 5731 elimasngOLD 6078 funopg 6571 f1osng 6861 fsng 7119 fnpr2g 7196 unexb 7718 op1stg 7969 op2ndg 7970 xpsneng 9039 xpcomeng 9047 sbth 9076 sbthfi 9185 unxpdom 9236 fpwwe2lem4 10611 prcdnq 10970 mhmlem 18917 carsgmon 33144 brimageg 34729 brdomaing 34737 brrangeg 34738 rankung 34968 mbfresfi 36338 zindbi 41456 2sbc6g 42945 2sbc5g 42946 fmulcl 44070 |
Copyright terms: Public domain | W3C validator |