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 2751 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | nfcv 2751 | . 2 ⊢ Ⅎ𝑦𝐵 | |
4 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | nfv 1830 | . 2 ⊢ Ⅎ𝑦𝜒 | |
6 | vtocl2g.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
7 | vtocl2g.2 | . 2 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
8 | vtocl2g.3 | . 2 ⊢ 𝜑 | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | vtocl2gf 3241 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 |
This theorem is referenced by: vtocl4g 3250 ifexg 4107 uniprg 4386 intprg 4446 opthg 4872 opelopabsb 4910 vtoclr 5086 elimasng 5410 cnvsng 5539 funopg 5836 f1osng 6089 fsng 6310 fvsng 6352 fnpr2g 6379 unexb 6856 op1stg 7071 op2ndg 7072 xpsneng 7930 xpcomeng 7937 sbth 7965 unxpdom 8052 fpwwe2lem5 9335 prcdnq 9694 mhmlem 17358 2pthoncl 26133 carsgmon 29703 br1steqg 30919 br2ndeqg 30920 brimageg 31204 brdomaing 31212 brrangeg 31213 rankung 31443 mbfresfi 32626 zindbi 36529 2sbc6g 37638 2sbc5g 37639 fmulcl 38648 |
Copyright terms: Public domain | W3C validator |