Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vtocl2ga | Structured version Visualization version GIF version |
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2144 and ax-11 2160. (Revised by Gino Giotto, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.) |
Ref | Expression |
---|---|
vtocl2ga.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtocl2ga.2 | ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
vtocl2ga.3 | ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) |
Ref | Expression |
---|---|
vtocl2ga | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtocl2ga.2 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | |
2 | 1 | imbi2d 343 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝐶 → 𝜓) ↔ (𝐴 ∈ 𝐶 → 𝜒))) |
3 | vtocl2ga.1 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | imbi2d 343 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑦 ∈ 𝐷 → 𝜑) ↔ (𝑦 ∈ 𝐷 → 𝜓))) |
5 | vtocl2ga.3 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) | |
6 | 5 | ex 415 | . . . . 5 ⊢ (𝑥 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜑)) |
7 | 4, 6 | vtoclga 3577 | . . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓)) |
8 | 7 | com12 32 | . . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓)) |
9 | 2, 8 | vtoclga 3577 | . 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒)) |
10 | 9 | impcom 410 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1536 ∈ wcel 2113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1780 df-cleq 2817 df-clel 2896 |
This theorem is referenced by: solin 5501 caovcan 7355 pwfseqlem2 10084 mulcanenq 10385 ltaddnq 10399 ltrnq 10404 genpv 10424 wrdind 14087 fsumrelem 15165 imasleval 16817 fullfunc 17179 fthfunc 17180 symggrplem 18052 pf1ind 20521 mretopd 21703 dvlip 24593 scvxcvx 25566 issubgoilem 29040 cnre2csqlem 31157 |
Copyright terms: Public domain | W3C validator |