![]() |
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 | nfv 1883 | . 2 ⊢ Ⅎ𝑥𝜒 | |
2 | nfv 1883 | . 2 ⊢ Ⅎ𝑦𝜓 | |
3 | rspc2v.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
4 | rspc2v.2 | . 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | rspc2 3351 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-v 3233 |
This theorem is referenced by: rspc2va 3354 rspc3v 3356 disji2 4668 f1veqaeq 6554 isorel 6616 isosolem 6637 oveqrspc2v 6713 fovcl 6807 caovclg 6868 caovcomg 6871 smoel 7502 fiint 8278 dffi3 8378 ltordlem 10591 seqhomo 12888 cshf1 13602 climcn2 14367 drsdir 16982 tsrlin 17266 dirge 17284 mhmlin 17389 issubg2 17656 nsgbi 17672 ghmlin 17712 efgi 18178 efgred 18207 irredmul 18755 issubrg2 18848 abvmul 18877 abvtri 18878 lmodlema 18916 islmodd 18917 rmodislmodlem 18978 rmodislmod 18979 lmhmlin 19083 lbsind 19128 mplcoe5lem 19515 ipcj 20027 obsip 20113 matecl 20279 dmatelnd 20350 scmateALT 20366 mdetdiaglem 20452 mdetdiagid 20454 pmatcoe1fsupp 20554 m2cpminvid2lem 20607 inopn 20752 basis1 20802 basis2 20803 iscldtop 20947 hausnei 21180 t1sep2 21221 nconnsubb 21274 r0sep 21599 fbasssin 21687 fcfneii 21888 ustssel 22056 xmeteq0 22190 tngngp3 22507 nmvs 22527 cncfi 22744 c1lip1 23805 aalioulem3 24134 logltb 24391 cvxcl 24756 2sqlem8 25196 axtgcgrrflx 25406 axtgsegcon 25408 axtg5seg 25409 axtgbtwnid 25410 axtgpasch 25411 axtgcont1 25412 axtgupdim2 25415 axtgeucl 25416 iscgrglt 25454 isperp2d 25656 f1otrgds 25794 brbtwn2 25830 axcontlem3 25891 axcontlem9 25897 axcontlem10 25898 upgrwlkdvdelem 26688 conngrv2edg 27173 frgrwopreglem5ALT 27302 ablocom 27530 nvs 27646 nvtri 27653 phpar2 27806 phpar 27807 shaddcl 28202 shmulcl 28203 cnopc 28900 unop 28902 hmop 28909 cnfnc 28917 adj1 28920 hstel2 29206 stj 29222 stcltr1i 29261 mddmdin0i 29418 cdj3lem1 29421 cdj3lem2b 29424 disji2f 29516 disjif2 29520 disjxpin 29527 fovcld 29568 isoun 29607 archirng 29870 archiexdiv 29872 slmdlema 29884 inelcarsg 30501 sibfof 30530 breprexplema 30836 axtgupdim2OLD 30874 pconncn 31332 nocvxminlem 32018 ivthALT 32455 poimirlem32 33571 ismtycnv 33731 ismtyima 33732 ismtyres 33737 bfplem1 33751 bfplem2 33752 ghomlinOLD 33817 rngohomadd 33898 rngohommul 33899 crngocom 33930 idladdcl 33948 idllmulcl 33949 idlrmulcl 33950 pridl 33966 ispridlc 33999 pridlc 34000 dmnnzd 34004 oposlem 34787 omllaw 34848 hlsuprexch 34985 lautle 35688 ltrnu 35725 tendovalco 36370 ntrkbimka 38653 mullimc 40166 mullimcf 40173 lptre2pt 40190 fourierdlem54 40695 faovcl 41601 icceuelpartlem 41696 iccpartnel 41699 fargshiftf1 41702 sprsymrelfolem2 42068 mgmhmlin 42111 issubmgm2 42115 |
Copyright terms: Public domain | W3C validator |