![]() |
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 3592 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
4 | 3 | imp 408 | 1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 |
This theorem is referenced by: swopo 5560 soisores 7276 soisoi 7277 isocnv 7279 isotr 7285 ovrspc2v 7387 caofrss 7657 caonncan 7662 frpoins3xpg 8076 coflton 8621 wunpr 10653 injresinj 13702 seqcaopr2 13953 rlimcn3 15481 o1of2 15504 isprm6 16598 ssc2 17713 pospropd 18224 tleile 18318 mhmpropd 18616 grpidssd 18831 grpinvssd 18832 dfgrp3lem 18853 isnsg3 18970 cyccom 19004 symgextf1 19211 efgredlemd 19534 efgredlem 19537 rglcom4d 19950 issrngd 20363 domneq0 20790 lindfind 21245 lindsind 21246 mplsubglem 21428 mdetunilem1 21984 mdetunilem3 21986 mdetunilem4 21987 mdetunilem9 21992 decpmatmulsumfsupp 22145 pm2mpf1 22171 pm2mpmhmlem1 22190 t0sep 22698 tsmsxplem2 23528 comet 23892 nrmmetd 23953 tngngp 24041 reconnlem2 24213 iscmet3lem1 24678 iscmet3lem2 24679 dchrisumlem1 26860 pntpbnd1 26957 ssltsepc 27161 tgjustc1 27466 tgjustc2 27467 iscgrglt 27505 motcgr 27527 perpneq 27705 foot 27713 f1otrg 27862 axcontlem10 27971 frgr2wwlk1 29322 orngmul 32152 lindsunlem 32383 mndpluscn 32571 unelros 32834 difelros 32835 inelsros 32841 diffiunisros 32842 cvxsconn 33901 elmrsubrn 34178 ghomco 36400 sticksstones10 40613 sticksstones12a 40615 fsuppind 40812 mzpcl34 41101 ntrk0kbimka 42403 isotone1 42412 isotone2 42413 nnfoctbdjlem 44786 isomuspgrlem2d 46113 mgmhmpropd 46169 rnghmmul 46288 2arymaptf1 46829 |
Copyright terms: Public domain | W3C validator |