![]() |
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 2139 and ax-11 2155. (Revised by GG, 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 340 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝐶 → 𝜓) ↔ (𝐴 ∈ 𝐶 → 𝜒))) |
3 | vtocl2ga.1 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | imbi2d 340 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑦 ∈ 𝐷 → 𝜑) ↔ (𝑦 ∈ 𝐷 → 𝜓))) |
5 | vtocl2ga.3 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑) | |
6 | 5 | ex 412 | . . . . 5 ⊢ (𝑥 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜑)) |
7 | 4, 6 | vtoclga 3577 | . . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓)) |
8 | 7 | com12 32 | . . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓)) |
9 | 2, 8 | vtoclga 3577 | . 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒)) |
10 | 9 | impcom 407 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 |
This theorem is referenced by: vtocl3ga 3583 vtocl4ga 3586 solin 5623 caovcan 7637 xpord2pred 8169 pwfseqlem2 10697 mulcanenq 10998 ltaddnq 11012 ltrnq 11017 genpv 11037 wrdind 14757 fsumrelem 15840 imasleval 17588 fullfunc 17960 fthfunc 17961 symggrplem 18910 pf1ind 22375 mretopd 23116 dvlip 26047 scvxcvx 27044 issubgoilem 31289 cnre2csqlem 33871 |
Copyright terms: Public domain | W3C validator |