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 3570 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
4 | 3 | imp 407 | 1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∀wral 3064 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 |
This theorem is referenced by: swopo 5514 soisores 7198 soisoi 7199 isocnv 7201 isotr 7207 ovrspc2v 7301 caofrss 7569 caonncan 7574 wunpr 10465 injresinj 13508 seqcaopr2 13759 rlimcn3 15299 o1of2 15322 isprm6 16419 ssc2 17534 pospropd 18045 tleile 18139 mhmpropd 18436 grpidssd 18651 grpinvssd 18652 dfgrp3lem 18673 isnsg3 18788 cyccom 18822 symgextf1 19029 efgredlemd 19350 efgredlem 19353 issrngd 20121 domneq0 20568 lindfind 21023 lindsind 21024 mplsubglem 21205 mdetunilem1 21761 mdetunilem3 21763 mdetunilem4 21764 mdetunilem9 21769 decpmatmulsumfsupp 21922 pm2mpf1 21948 pm2mpmhmlem1 21967 t0sep 22475 tsmsxplem2 23305 comet 23669 nrmmetd 23730 tngngp 23818 reconnlem2 23990 iscmet3lem1 24455 iscmet3lem2 24456 dchrisumlem1 26637 pntpbnd1 26734 tgjustc1 26836 tgjustc2 26837 iscgrglt 26875 motcgr 26897 perpneq 27075 foot 27083 f1otrg 27232 axcontlem10 27341 frgr2wwlk1 28693 orngmul 31502 lindsunlem 31705 mndpluscn 31876 unelros 32139 difelros 32140 inelsros 32146 diffiunisros 32147 cvxsconn 33205 elmrsubrn 33482 frpoins3xpg 33787 ssltsepc 33987 ghomco 36049 sticksstones10 40111 sticksstones12a 40113 fsuppind 40279 mzpcl34 40553 ntrk0kbimka 41649 isotone1 41658 isotone2 41659 nnfoctbdjlem 43993 isomuspgrlem2d 45283 mgmhmpropd 45339 rnghmmul 45458 2arymaptf1 45999 |
Copyright terms: Public domain | W3C validator |