| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspc2v | Structured version Visualization version GIF version | ||
| Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
| Ref | Expression |
|---|---|
| rspc2v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
| rspc2v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rspc2v | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspc2v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 2 | 1 | ralbidv 3152 | . . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒)) |
| 3 | 2 | rspcv 3573 | . 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒)) |
| 4 | rspc2v.2 | . . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
| 5 | 4 | rspcv 3573 | . 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓)) |
| 6 | 3, 5 | sylan9 507 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ral 3045 |
| This theorem is referenced by: rspc2va 3589 rspc3v 3593 rspc6v 3598 disji2 5076 f1veqaeq 7193 isorel 7263 isosolem 7284 oveqrspc2v 7376 fovcld 7476 caovclg 7541 caovcomg 7544 caofidlcan 7651 resf1extb 7867 smoel 8283 fiint 9216 fiintOLD 9217 dffi3 9321 ltordlem 11645 seqhomo 13956 cshf1 14716 climcn2 15500 drsdir 18208 tsrlin 18491 dirge 18509 mgmhmlin 18573 issubmgm2 18577 mhmlin 18667 issubg2 19020 nsgbi 19036 ghmlin 19100 efgi 19598 efgred 19627 rglcom4d 20096 irredmul 20314 issubrng2 20443 issubrg2 20477 abvmul 20706 abvtri 20707 lmodlema 20768 islmodd 20769 rmodislmodlem 20832 rmodislmod 20833 lmhmlin 20939 lbsind 20984 rnglidlmcl 21123 ipcj 21541 obsip 21628 mplcoe5lem 21944 matecl 22310 dmatelnd 22381 scmateALT 22397 mdetdiaglem 22483 mdetdiagid 22485 pmatcoe1fsupp 22586 m2cpminvid2lem 22639 inopn 22784 basis1 22835 basis2 22836 iscldtop 22980 hausnei 23213 t1sep2 23254 nconnsubb 23308 r0sep 23633 fbasssin 23721 fcfneii 23922 ustssel 24091 xmeteq0 24224 tngngp3 24542 nmvs 24562 cncfi 24785 c1lip1 25900 aalioulem3 26240 logltb 26507 cvxcl 26893 2sqlem8 27335 nocvxminlem 27688 madebday 27814 negsproplem1 27939 negsprop 27946 axtgcgrrflx 28407 axtgsegcon 28409 axtg5seg 28410 axtgbtwnid 28411 axtgpasch 28412 axtgcont1 28413 axtgupdim2 28416 axtgeucl 28417 isperp2d 28661 f1otrgds 28814 brbtwn2 28850 axcontlem3 28911 axcontlem9 28917 axcontlem10 28918 upgrwlkdvdelem 29681 conngrv2edg 30139 frgrwopreglem5ALT 30266 ablocom 30492 nvs 30607 nvtri 30614 phpar2 30767 phpar 30768 shaddcl 31161 shmulcl 31162 cnopc 31857 unop 31859 hmop 31866 cnfnc 31874 adj1 31877 hstel2 32163 stj 32179 stcltr1i 32218 mddmdin0i 32375 cdj3lem1 32378 cdj3lem2b 32381 disji2f 32521 disjif2 32525 disjxpin 32532 isoun 32645 archirng 33131 archiexdiv 33133 slmdlema 33146 inelcarsg 34285 sibfof 34314 breprexplema 34604 axtgupdim2ALTV 34642 pconncn 35207 ivthALT 36319 poimirlem32 37642 ismtycnv 37792 ismtyima 37793 ismtyres 37798 bfplem1 37812 bfplem2 37813 ghomlinOLD 37878 rngohomadd 37959 rngohommul 37960 crngocom 37991 idladdcl 38009 idllmulcl 38010 idlrmulcl 38011 pridl 38027 ispridlc 38060 pridlc 38061 dmnnzd 38065 oposlem 39171 omllaw 39232 hlsuprexch 39370 lautle 40073 ltrnu 40110 tendovalco 40754 sticksstones1 42129 sticksstones2 42130 ntrkbimka 44021 relprel 44935 mullimc 45607 mullimcf 45614 lptre2pt 45631 fourierdlem54 46151 fcoresf1 47063 faovcl 47194 icceuelpartlem 47429 iccpartnel 47432 fargshiftf1 47435 sprsymrelfolem2 47487 reuopreuprim 47520 isubgr3stgrlem6 47965 isthincd2lem2 49430 |
| Copyright terms: Public domain | W3C validator |