HomeHome Intuitionistic Logic Explorer
Theorem List (p. 45 of 73)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremxpriindim 4401* Distributive law for cross product over relativized indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
(y y A → (𝐶 × (𝐷 x A B)) = ((𝐶 × 𝐷) ∩ x A (𝐶 × B)))
 
Theoremeliunxp 4402* Membership in a union of cross products. Analogue of elxp 4289 for nonconstant B(x). (Contributed by Mario Carneiro, 29-Dec-2014.)
(𝐶 x A ({x} × B) ↔ xy(𝐶 = ⟨x, y (x A y B)))
 
Theoremopeliunxp2 4403* Membership in a union of cross products. (Contributed by Mario Carneiro, 14-Feb-2015.)
(x = 𝐶B = 𝐸)       (⟨𝐶, 𝐷 x A ({x} × B) ↔ (𝐶 A 𝐷 𝐸))
 
Theoremraliunxp 4404* Write a double restricted quantification as one universal quantifier. In this version of ralxp 4406, B(y) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
(x = ⟨y, z⟩ → (φψ))       (x y A ({y} × B)φy A z B ψ)
 
Theoremrexiunxp 4405* Write a double restricted quantification as one universal quantifier. In this version of rexxp 4407, B(y) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
(x = ⟨y, z⟩ → (φψ))       (x y A ({y} × B)φy A z B ψ)
 
Theoremralxp 4406* Universal quantification restricted to a cross product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
(x = ⟨y, z⟩ → (φψ))       (x (A × B)φy A z B ψ)
 
Theoremrexxp 4407* Existential quantification restricted to a cross product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
(x = ⟨y, z⟩ → (φψ))       (x (A × B)φy A z B ψ)
 
Theoremdjussxp 4408* Disjoint union is a subset of a cross product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
x A ({x} × B) ⊆ (A × V)
 
Theoremralxpf 4409* Version of ralxp 4406 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
yφ    &   zφ    &   xψ    &   (x = ⟨y, z⟩ → (φψ))       (x (A × B)φy A z B ψ)
 
Theoremrexxpf 4410* Version of rexxp 4407 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
yφ    &   zφ    &   xψ    &   (x = ⟨y, z⟩ → (φψ))       (x (A × B)φy A z B ψ)
 
Theoremiunxpf 4411* Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
y𝐶    &   z𝐶    &   x𝐷    &   (x = ⟨y, z⟩ → 𝐶 = 𝐷)        x (A × B)𝐶 = y A z B 𝐷
 
Theoremopabbi2dv 4412* Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2138. (Contributed by NM, 24-Feb-2014.)
Rel A    &   (φ → (⟨x, y Aψ))       (φA = {⟨x, y⟩ ∣ ψ})
 
Theoremrelop 4413* A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
A V    &   B V       (Rel ⟨A, B⟩ ↔ xy(A = {x} B = {x, y}))
 
Theoremideqg 4414 For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(B 𝑉 → (A I BA = B))
 
Theoremideq 4415 For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
B V       (A I BA = B)
 
Theoremididg 4416 A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(A 𝑉A I A)
 
Theoremissetid 4417 Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
(A V ↔ A I A)
 
Theoremcoss1 4418 Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
(AB → (A𝐶) ⊆ (B𝐶))
 
Theoremcoss2 4419 Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
(AB → (𝐶A) ⊆ (𝐶B))
 
Theoremcoeq1 4420 Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
(A = B → (A𝐶) = (B𝐶))
 
Theoremcoeq2 4421 Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
(A = B → (𝐶A) = (𝐶B))
 
Theoremcoeq1i 4422 Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
A = B       (A𝐶) = (B𝐶)
 
Theoremcoeq2i 4423 Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
A = B       (𝐶A) = (𝐶B)
 
Theoremcoeq1d 4424 Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
(φA = B)       (φ → (A𝐶) = (B𝐶))
 
Theoremcoeq2d 4425 Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
(φA = B)       (φ → (𝐶A) = (𝐶B))
 
Theoremcoeq12i 4426 Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
A = B    &   𝐶 = 𝐷       (A𝐶) = (B𝐷)
 
Theoremcoeq12d 4427 Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
(φA = B)    &   (φ𝐶 = 𝐷)       (φ → (A𝐶) = (B𝐷))
 
Theoremnfco 4428 Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
xA    &   xB       x(AB)
 
Theorembrcog 4429* Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
((A 𝑉 B 𝑊) → (A(𝐶𝐷)Bx(A𝐷x x𝐶B)))
 
Theoremopelco2g 4430* Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
((A 𝑉 B 𝑊) → (⟨A, B (𝐶𝐷) ↔ x(⟨A, x 𝐷 x, B 𝐶)))
 
Theorembrcogw 4431 Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
(((A 𝑉 B 𝑊 𝑋 𝑍) (A𝐷𝑋 𝑋𝐶B)) → A(𝐶𝐷)B)
 
Theoremeqbrrdva 4432* Deduction from extensionality principle for relations, given an equivalence only on the relation's domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
(φA ⊆ (𝐶 × 𝐷))    &   (φB ⊆ (𝐶 × 𝐷))    &   ((φ x 𝐶 y 𝐷) → (xAyxBy))       (φA = B)
 
Theorembrco 4433* Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
A V    &   B V       (A(𝐶𝐷)Bx(A𝐷x x𝐶B))
 
Theoremopelco 4434* Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
A V    &   B V       (⟨A, B (𝐶𝐷) ↔ x(A𝐷x x𝐶B))
 
Theoremcnvss 4435 Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
(ABAB)
 
Theoremcnveq 4436 Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
(A = BA = B)
 
Theoremcnveqi 4437 Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
A = B       A = B
 
Theoremcnveqd 4438 Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
(φA = B)       (φA = B)
 
Theoremelcnv 4439* Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
(A 𝑅xy(A = ⟨x, y y𝑅x))
 
Theoremelcnv2 4440* Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
(A 𝑅xy(A = ⟨x, yy, x 𝑅))
 
Theoremnfcnv 4441 Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA       xA
 
Theoremopelcnvg 4442 Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
((A 𝐶 B 𝐷) → (⟨A, B 𝑅 ↔ ⟨B, A 𝑅))
 
Theorembrcnvg 4443 The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
((A 𝐶 B 𝐷) → (A𝑅BB𝑅A))
 
Theoremopelcnv 4444 Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
A V    &   B V       (⟨A, B 𝑅 ↔ ⟨B, A 𝑅)
 
Theorembrcnv 4445 The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
A V    &   B V       (A𝑅BB𝑅A)
 
Theoremcsbcnvg 4446 Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
(A 𝑉A / x𝐹 = A / x𝐹)
 
Theoremcnvco 4447 Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(AB) = (BA)
 
Theoremcnvuni 4448* The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
A = x A x
 
Theoremdfdm3 4449* Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
dom A = {xyx, y A}
 
Theoremdfrn2 4450* Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
ran A = {yx xAy}
 
Theoremdfrn3 4451* Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
ran A = {yxx, y A}
 
Theoremelrn2g 4452* Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
(A 𝑉 → (A ran Bxx, A B))
 
Theoremelrng 4453* Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
(A 𝑉 → (A ran Bx xBA))
 
Theoremdfdm4 4454 Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
dom A = ran A
 
Theoremdfdmf 4455* Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA    &   yA       dom A = {xy xAy}
 
Theoremcsbdmg 4456 Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
(A 𝑉A / xdom B = dom A / xB)
 
Theoremeldmg 4457* Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
(A 𝑉 → (A dom By ABy))
 
Theoremeldm2g 4458* Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
(A 𝑉 → (A dom ByA, y B))
 
Theoremeldm 4459* Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
A V       (A dom By ABy)
 
Theoremeldm2 4460* Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
A V       (A dom ByA, y B)
 
Theoremdmss 4461 Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
(AB → dom A ⊆ dom B)
 
Theoremdmeq 4462 Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
(A = B → dom A = dom B)
 
Theoremdmeqi 4463 Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
A = B       dom A = dom B
 
Theoremdmeqd 4464 Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
(φA = B)       (φ → dom A = dom B)
 
Theoremopeldm 4465 Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
A V    &   B V       (⟨A, B 𝐶A dom 𝐶)
 
Theorembreldm 4466 Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
A V    &   B V       (A𝑅BA dom 𝑅)
 
Theoremopeldmg 4467 Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
((A 𝑉 B 𝑊) → (⟨A, B 𝐶A dom 𝐶))
 
Theorembreldmg 4468 Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
((A 𝐶 B 𝐷 A𝑅B) → A dom 𝑅)
 
Theoremdmun 4469 The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
dom (AB) = (dom A ∪ dom B)
 
Theoremdmin 4470 The domain of an intersection belong to the intersection of domains. Theorem 6 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
dom (AB) ⊆ (dom A ∩ dom B)
 
Theoremdmiun 4471 The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
dom x A B = x A dom B
 
Theoremdmuni 4472* The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
dom A = x A dom x
 
Theoremdmopab 4473* The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
dom {⟨x, y⟩ ∣ φ} = {xyφ}
 
Theoremdmopabss 4474* Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
dom {⟨x, y⟩ ∣ (x A φ)} ⊆ A
 
Theoremdmopab3 4475* The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
(x A yφ ↔ dom {⟨x, y⟩ ∣ (x A φ)} = A)
 
Theoremdm0 4476 The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
dom ∅ = ∅
 
Theoremdmi 4477 The domain of the identity relation is the universe. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
dom I = V
 
Theoremdmv 4478 The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
dom V = V
 
Theoremdm0rn0 4479 An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
(dom A = ∅ ↔ ran A = ∅)
 
Theoremreldm0 4480 A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
(Rel A → (A = ∅ ↔ dom A = ∅))
 
Theoremdmmrnm 4481* A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
(x x dom Ay y ran A)
 
Theoremdmxpm 4482* The domain of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(x x B → dom (A × B) = A)
 
Theoremdmxpinm 4483* The domain of the intersection of two square cross products. Unlike dmin 4470, equality holds. (Contributed by NM, 29-Jan-2008.)
(x x (AB) → dom ((A × A) ∩ (B × B)) = (AB))
 
Theoremxpid11m 4484* The cross product of a class with itself is one-to-one. (Contributed by Jim Kingdon, 8-Dec-2018.)
((x x A x x B) → ((A × A) = (B × B) ↔ A = B))
 
Theoremdmcnvcnv 4485 The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 4698). (Contributed by NM, 8-Apr-2007.)
dom A = dom A
 
Theoremrncnvcnv 4486 The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
ran A = ran A
 
Theoremelreldm 4487 The first member of an ordered pair in a relation belongs to the domain of the relation. (Contributed by NM, 28-Jul-2004.)
((Rel A B A) → B dom A)
 
Theoremrneq 4488 Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
(A = B → ran A = ran B)
 
Theoremrneqi 4489 Equality inference for range. (Contributed by NM, 4-Mar-2004.)
A = B       ran A = ran B
 
Theoremrneqd 4490 Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
(φA = B)       (φ → ran A = ran B)
 
Theoremrnss 4491 Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
(AB → ran A ⊆ ran B)
 
Theorembrelrng 4492 The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.)
((A 𝐹 B 𝐺 A𝐶B) → B ran 𝐶)
 
Theoremopelrng 4493 Membership of second member of an ordered pair in a range. (Contributed by Jim Kingdon, 26-Jan-2019.)
((A 𝐹 B 𝐺 A, B 𝐶) → B ran 𝐶)
 
Theorembrelrn 4494 The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
A V    &   B V       (A𝐶BB ran 𝐶)
 
Theoremopelrn 4495 Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.)
A V    &   B V       (⟨A, B 𝐶B ran 𝐶)
 
Theoremreleldm 4496 The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)
((Rel 𝑅 A𝑅B) → A dom 𝑅)
 
Theoremrelelrn 4497 The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.)
((Rel 𝑅 A𝑅B) → B ran 𝑅)
 
Theoremreleldmb 4498* Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
(Rel 𝑅 → (A dom 𝑅x A𝑅x))
 
Theoremrelelrnb 4499* Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
(Rel 𝑅 → (A ran 𝑅x x𝑅A))
 
Theoremreleldmi 4500 The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
Rel 𝑅       (A𝑅BA dom 𝑅)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7215
  Copyright terms: Public domain < Previous  Next >