|   | 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 2141 and ax-11 2157. (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 1540 ∈ wcel 2108 | 
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 | 
| This theorem is referenced by: vtocl3ga 3583 vtocl4ga 3586 solin 5619 caovcan 7637 xpord2pred 8170 pwfseqlem2 10699 mulcanenq 11000 ltaddnq 11014 ltrnq 11019 genpv 11039 wrdind 14760 fsumrelem 15843 imasleval 17586 fullfunc 17953 fthfunc 17954 symggrplem 18897 pf1ind 22359 mretopd 23100 dvlip 26032 scvxcvx 27029 issubgoilem 31279 cnre2csqlem 33909 | 
| Copyright terms: Public domain | W3C validator |