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 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 3450 | . 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 3505 | . . 3 ⊢ (𝐴 ∈ V → 𝜓) |
7 | 3, 6 | vtoclg 3505 | . 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒)) |
8 | 1, 7 | mpan9 507 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 Vcvv 3432 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 |
This theorem is referenced by: vtocl3g 3511 vtocl4g 3519 uniprgOLD 4859 intprgOLD 4915 opthg 5392 opelopabsb 5443 vtoclr 5650 elimasngOLD 5998 funopg 6468 f1osng 6757 fsng 7009 fnpr2g 7086 unexb 7598 op1stg 7843 op2ndg 7844 xpsneng 8843 xpcomeng 8851 sbth 8880 sbthfi 8985 unxpdom 9030 fpwwe2lem4 10390 prcdnq 10749 mhmlem 18695 carsgmon 32281 brimageg 34229 brdomaing 34237 brrangeg 34238 rankung 34468 mbfresfi 35823 zindbi 40768 2sbc6g 42033 2sbc5g 42034 fmulcl 43122 |
Copyright terms: Public domain | W3C validator |