![]() |
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.) |
Ref | Expression |
---|---|
vtocl2g.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl2g.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
vtocl2g.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl2g | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2913 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2913 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | nfcv 2913 | . 2 ⊢ Ⅎ𝑦𝐵 | |
4 | nfv 1995 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | nfv 1995 | . 2 ⊢ Ⅎ𝑦𝜒 | |
6 | vtocl2g.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
7 | vtocl2g.2 | . 2 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
8 | vtocl2g.3 | . 2 ⊢ 𝜑 | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | vtocl2gf 3419 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1631 ∈ wcel 2145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 |
This theorem is referenced by: vtocl4g 3428 ifexg 4296 uniprg 4588 intprg 4645 opthg 5073 opelopabsb 5118 vtoclr 5304 elimasng 5632 cnvsngOLD 5765 funopg 6065 f1osng 6318 fsng 6547 fvsng 6591 fnpr2g 6618 unexb 7105 op1stg 7327 op2ndg 7328 xpsneng 8201 xpcomeng 8208 sbth 8236 unxpdom 8323 fpwwe2lem5 9658 prcdnq 10017 mhmlem 17743 carsgmon 30716 br1steqgOLD 32010 br2ndeqgOLD 32011 brimageg 32371 brdomaing 32379 brrangeg 32380 rankung 32610 mbfresfi 33788 zindbi 38037 2sbc6g 39142 2sbc5g 39143 fmulcl 40331 |
Copyright terms: Public domain | W3C validator |