![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rspc2v | 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 1473 | . 2 ⊢ Ⅎ𝑥𝜒 | |
2 | nfv 1473 | . 2 ⊢ Ⅎ𝑦𝜓 | |
3 | rspc2v.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
4 | rspc2v.2 | . 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | rspc2 2746 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1296 ∈ wcel 1445 ∀wral 2370 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-v 2635 |
This theorem is referenced by: rspc2va 2749 rspc3v 2751 disji2 3860 wetriext 4420 f1veqaeq 5586 isorel 5625 fovcl 5788 caovclg 5835 caovcomg 5838 smoel 6103 dcdifsnid 6303 unfiexmid 6708 fiintim 6719 supmoti 6768 supsnti 6780 isotilem 6781 cauappcvgprlem1 7315 caucvgprlemnkj 7322 caucvgprlemnbj 7323 caucvgprprlemval 7344 ltordlem 8057 frecuzrdgrrn 9964 frec2uzrdg 9965 frecuzrdgrcl 9966 frecuzrdgrclt 9971 seq3caopr3 10047 seq3homo 10076 climcn2 10868 inopn 11870 basis1 11913 basis2 11914 xmeteq0 12161 cncfi 12347 |
Copyright terms: Public domain | W3C validator |