![]() |
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 2138 and ax-11 2155. (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 341 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝐶 → 𝜓) ↔ (𝐴 ∈ 𝐶 → 𝜒))) |
3 | vtocl2ga.1 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | imbi2d 341 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑦 ∈ 𝐷 → 𝜑) ↔ (𝑦 ∈ 𝐷 → 𝜓))) |
5 | vtocl2ga.3 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) | |
6 | 5 | ex 414 | . . . . 5 ⊢ (𝑥 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜑)) |
7 | 4, 6 | vtoclga 3536 | . . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓)) |
8 | 7 | com12 32 | . . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓)) |
9 | 2, 8 | vtoclga 3536 | . 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒)) |
10 | 9 | impcom 409 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 |
This theorem is referenced by: solin 5574 caovcan 7562 xpord2pred 8081 pwfseqlem2 10603 mulcanenq 10904 ltaddnq 10918 ltrnq 10923 genpv 10943 wrdind 14619 fsumrelem 15700 imasleval 17431 fullfunc 17801 fthfunc 17802 symggrplem 18702 pf1ind 21744 mretopd 22466 dvlip 25380 scvxcvx 26358 issubgoilem 30251 cnre2csqlem 32555 |
Copyright terms: Public domain | W3C validator |