| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspc2va | Structured version Visualization version GIF version | ||
| Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.) |
| Ref | Expression |
|---|---|
| rspc2v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
| rspc2v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rspc2va | ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspc2v.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 2 | rspc2v.2 | . . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
| 3 | 1, 2 | rspc2v 3633 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
| 4 | 3 | imp 406 | 1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∀wral 3061 |
| 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 df-ral 3062 |
| This theorem is referenced by: rspc2dv 3637 swopo 5603 f1ounsn 7292 soisores 7347 soisoi 7348 isocnv 7350 isotr 7356 ovrspc2v 7457 coof 7721 caofrss 7736 caonncan 7741 frpoins3xpg 8165 coflton 8709 wunpr 10749 injresinj 13827 seqcaopr2 14079 rlimcn3 15626 o1of2 15649 isprm6 16751 ssc2 17866 pospropd 18372 tleile 18466 mgmhmpropd 18711 mhmpropd 18805 grpidssd 19034 grpinvssd 19035 dfgrp3lem 19056 isnsg3 19178 cyccom 19221 symgextf1 19439 efgredlemd 19762 efgredlem 19765 rglcom4d 20208 rnghmmul 20449 domneq0 20708 issrngd 20856 lindfind 21836 lindsind 21837 mplsubglem 22019 mdetunilem1 22618 mdetunilem3 22620 mdetunilem4 22621 mdetunilem9 22626 decpmatmulsumfsupp 22779 pm2mpf1 22805 pm2mpmhmlem1 22824 t0sep 23332 tsmsxplem2 24162 comet 24526 nrmmetd 24587 tngngp 24675 reconnlem2 24849 iscmet3lem1 25325 iscmet3lem2 25326 dchrisumlem1 27533 pntpbnd1 27630 ssltsepc 27838 tgjustc1 28483 tgjustc2 28484 iscgrglt 28522 motcgr 28544 perpneq 28722 foot 28730 f1otrg 28879 axcontlem10 28988 frgr2wwlk1 30348 orngmul 33333 lindsunlem 33675 mndpluscn 33925 unelros 34172 difelros 34173 inelsros 34179 diffiunisros 34180 elmrsubrn 35525 ghomco 37898 sticksstones10 42156 sticksstones12a 42158 fsuppind 42600 mzpcl34 42742 ntrk0kbimka 44052 isotone1 44061 isotone2 44062 nnfoctbdjlem 46470 2arymaptf1 48574 |
| Copyright terms: Public domain | W3C validator |