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 2145, ax-11 2161, and ax-13 2390. (Revised by Steven Nguyen, 29-Nov-2022.) |
Ref | Expression |
---|---|
vtocl2g.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl2g.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
vtocl2g.3 | ⊢ 𝜑 |
Ref | Expression |
---|---|
vtocl2g | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3512 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | vtocl2g.2 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
3 | 2 | imbi2d 343 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ V → 𝜓) ↔ (𝐴 ∈ V → 𝜒))) |
4 | vtocl2g.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | vtocl2g.3 | . . . 4 ⊢ 𝜑 | |
6 | 4, 5 | vtoclg 3567 | . . 3 ⊢ (𝐴 ∈ V → 𝜓) |
7 | 3, 6 | vtoclg 3567 | . 2 ⊢ (𝐵 ∈ 𝑊 → (𝐴 ∈ V → 𝜒)) |
8 | 1, 7 | mpan9 509 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 Vcvv 3494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3496 |
This theorem is referenced by: vtocl4g 3579 uniprg 4856 intprg 4910 opthg 5369 opelopabsb 5417 vtoclr 5615 elimasng 5955 funopg 6389 f1osng 6655 fsng 6899 fnpr2g 6973 unexb 7471 op1stg 7701 op2ndg 7702 xpsneng 8602 xpcomeng 8609 sbth 8637 unxpdom 8725 fpwwe2lem5 10056 prcdnq 10415 mhmlem 18219 carsgmon 31572 brimageg 33388 brdomaing 33396 brrangeg 33397 rankung 33627 mbfresfi 34953 zindbi 39563 2sbc6g 40767 2sbc5g 40768 fmulcl 41882 |
Copyright terms: Public domain | W3C validator |