Metamath Proof Explorer - mmtheorems13

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 1201-1300 - Page 13 of 58

Type	Label	Description
Statement
Syntax	wral 1201	Extend wff notation to include restricted universal quantification.
wff ∀x ∈ A φ
Syntax	wrex 1202	Extend wff notation to include restricted existential quantification.
wff ∃x ∈ A φ
Syntax	wreu 1203	Extend wff notation to include restricted existential uniqueness.
wff ∃!x ∈ A φ
Syntax	crab 1204	Extend class notation to include restricted class abstractions.
class {x ∈ A∣φ}
Definition	df-ral 1205	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22.
⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
Definition	df-rex 1206	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.
⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
Definition	df-reu 1207	Define restricted existential uniqueness.
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
Definition	df-rab 1208	Define a restricted class abstraction, which is the class of all x in A such that φ is true. Definition of [TakeutiZaring] p. 20.
⊢ {x ∈ A∣φ} = {x∣(x ∈ A ∧ φ)}
Theorem	ralnex 1209	Relationship between restricted universal and existential quantifiers.
⊢ (∀x ∈ A ¬ φ ↔ ¬ ∃x ∈ A φ)
Theorem	rexnal 1210	Relationship between restricted universal and existential quantifiers.
⊢ (∃x ∈ A ¬ φ ↔ ¬ ∀x ∈ A φ)
Theorem	dfral2 1211	Relationship between restricted universal and existential quantifiers.
⊢ (∀x ∈ A φ ↔ ¬ ∃x ∈ A ¬ φ)
Theorem	dfrex2 1212	Relationship between restricted universal and existential quantifiers.
⊢ (∃x ∈ A φ ↔ ¬ ∀x ∈ A ¬ φ)
Theorem	biralda 1213	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	birexda 1214	Formula-building rule for restricted existential quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	biraldva 1215	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	birexdva 1216	Formula-building rule for restricted existential quantifier (deduction rule).
⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	birald 1217	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	birexd 1218	Formula-building rule for restricted existential quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	biraldv 1219	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	birexdv 1220	Formula-building rule for restricted existential quantifier (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	biraldv2 1221	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ (φ → ((x ∈ A → ψ) ↔ (x ∈ B → χ)))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B χ))
Theorem	birexdv2 1222	Formula-building rule for restricted existential quantifier (deduction rule).
⊢ (φ → ((x ∈ A ∧ ψ) ↔ (x ∈ B ∧ χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ B χ))
Theorem	biral 1223	Inference adding restricted universal quantifier to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)
Theorem	birex 1224	Inference adding restricted existential quantifier to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)
Theorem	bi2ral 1225	Inference adding 2 restricted universal quantifiers to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x ∈ A ∀y ∈ B ψ)
Theorem	bi2rex 1226	Inference adding 2 restricted existential quantifiers to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x ∈ A ∃y ∈ B ψ)
Theorem	birex2 1227	Inference adding different restricted existential quantifiers to each side of an equivalence.
⊢ ((x ∈ A ∧ φ) ↔ (x ∈ B ∧ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ B ψ)
Theorem	birala 1228	Inference adding restricted universal quantifier to both sides of an equivalence.
⊢ (x ∈ A → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)
Theorem	birexa 1229	Inference adding restricted existential quantifier to both sides of an equivalence.
⊢ (x ∈ A → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)
Theorem	bi2rexa 1230	Inference adding 2 restricted existential quantifiers to both sides of an equivalence.
⊢ ((x ∈ A ∧ y ∈ B) → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x ∈ A ∃y ∈ B ψ)
Theorem	r2al 1231	Double restricted universal quantification.
⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))
Theorem	bi2ralda 1232	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → ∀yφ)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	bi2raldva 1233	Formula-building rule for restricted universal quantifier (deduction rule).
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	bi2rexdva 1234	Formula-building rule for restricted existential quantifier (deduction rule).
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ ↔ ∃x ∈ A ∃y ∈ B χ))
Theorem	risset 1235	Two ways to say "A belongs to B".
⊢ (A ∈ B ↔ ∃x ∈ B x = A)
Theorem	hbral 1236	Bound-variable hypothesis builder for restricted quantification.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (φ → ∀xφ)    ⇒   ⊢ (∀y ∈ A φ → ∀x∀y ∈ A φ)
Theorem	hbra1 1237	x is not free in ∀x ∈ Aφ.
⊢ (∀x ∈ A φ → ∀x∀x ∈ A φ)
Theorem	hbrex 1238	Bound-variable hypothesis builder for restricted quantification.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (φ → ∀xφ)    ⇒   ⊢ (∃y ∈ A φ → ∀x∃y ∈ A φ)
Theorem	hbre1 1239	x is not free in ∃x ∈ Aφ.
⊢ (∃x ∈ A φ → ∀x∃x ∈ A φ)
Theorem	r3al 1240	Triple restricted universal quantification.
⊢ (∀x ∈ A ∀y ∈ B ∀z ∈ C φ ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ B ∧ z ∈ C) → φ))
Theorem	r2ex 1241	Double restricted existential quantification.
⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ))
Theorem	rexex 1242	Restricted existence implies existence.
⊢ (∃x ∈ A φ → ∃xφ)
Theorem	ra4 1243	Restricted specialization.
⊢ (∀x ∈ A φ → (x ∈ A → φ))
Theorem	ra4e 1244	Restricted specialization.
⊢ ((x ∈ A ∧ φ) → ∃x ∈ A φ)
Theorem	ra42 1245	Restricted specialization.
⊢ (∀x ∈ A ∀y ∈ B φ → ((x ∈ A ∧ y ∈ B) → φ))
Theorem	rspec 1246	Specialization rule for restricted quantification.
⊢ ∀x ∈ A φ    ⇒   ⊢ (x ∈ A → φ)
Theorem	rgen 1247	Generalization rule for restricted quantification.
⊢ (x ∈ A → φ)    ⇒   ⊢ ∀x ∈ A φ
Theorem	rgen2 1248	Generalization rule for restricted quantification. Note that x and y needn't be distinct.
⊢ ((x ∈ A ∧ y ∈ A) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ A φ
Theorem	mprg 1249	Modus ponens combined with restricted generalization.
⊢ (∀x ∈ A φ → ψ)    &   ⊢ (x ∈ A → φ)    ⇒   ⊢ ψ
Theorem	mprgbir 1250	Modus ponens on biconditional combined with restricted generalization.
⊢ (φ ↔ ∀x ∈ A ψ)    &   ⊢ (x ∈ A → ψ)    ⇒   ⊢ φ
Theorem	r19.20 1251	Distribution of restricted quantification over implication.
⊢ (∀x ∈ A (φ → ψ) → (∀x ∈ A φ → ∀x ∈ A ψ))
Theorem	r19.20i2 1252	Inference quantifying both antecedent and consequent.
⊢ ((x ∈ A → φ) → (x ∈ B → ψ))    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ B ψ)
Theorem	r19.20i 1253	Inference quantifying both antecedent and consequent.
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	r19.20si 1254	Inference quantifying both antecedent and consequent, with strong hypothesis.
⊢ (φ → ψ)    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	r19.20da 1255	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    &   ⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	r19.20dva 1256	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	r19.20sdv 1257	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	r19.21ai 1258	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (x ∈ A → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	r19.21aiv 1259	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → (x ∈ A → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	r19.21v 1260	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers.
⊢ (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ))
Theorem	r19.21ad 1261	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (φ → (ψ → (x ∈ A → χ)))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A χ))
Theorem	r19.21adv 1262	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → (ψ → (x ∈ A → χ)))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A χ))
Theorem	r19.21aivv 1263	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
⊢ (φ → ((x ∈ A ∧ y ∈ B) → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ∀y ∈ B ψ)
Theorem	rgen2a 1264	Generalization rule for restricted quantification.
⊢ ((x ∈ A ∧ y ∈ B) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ B φ
Theorem	rgen3 1265	Generalization rule for restricted quantification.
⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ A ∀z ∈ A φ
Theorem	r19.21bi 1266	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ∀x ∈ A ψ)    ⇒   ⊢ ((φ ∧ x ∈ A) → ψ)
Theorem	rspec2 1267	Specialization rule for restricted quantification.
⊢ ∀x ∈ A ∀y ∈ B φ    ⇒   ⊢ ((x ∈ A ∧ y ∈ B) → φ)
Theorem	rspec3 1268	Specialization rule for restricted quantification.
⊢ ∀x ∈ A ∀y ∈ B ∀z ∈ C φ    ⇒   ⊢ ((x ∈ A ∧ y ∈ B ∧ z ∈ C) → φ)
Theorem	r19.21be 1269	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ∀x ∈ A ψ)    ⇒   ⊢ ∀x ∈ A (φ → ψ)
Theorem	nrex 1270	Inference adding restricted existential quantifier to negated wff.
⊢ (x ∈ A → ¬ ψ)    ⇒   ⊢ ¬ ∃x ∈ A ψ
Theorem	nrexdv 1271	Deduction adding restricted existential quantifier to negated wff.
⊢ ((φ ∧ x ∈ A) → ¬ ψ)    ⇒   ⊢ (φ → ¬ ∃x ∈ A ψ)
Theorem	r19.22 1272	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (∀x ∈ A (φ → ψ) → (∃x ∈ A φ → ∃x ∈ A ψ))
Theorem	r19.22i 1273	Inference quantifying both antecedent and consequent.
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∃x ∈ A φ → ∃x ∈ A ψ)
Theorem	r19.22i2 1274	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
⊢ ((x ∈ A ∧ φ) → (x ∈ B ∧ ψ))    ⇒   ⊢ (∃x ∈ A φ → ∃x ∈ B ψ)
Theorem	r19.22si 1275	Inference quantifying both antecedent and consequent.
⊢ (φ → ψ)    ⇒   ⊢ (∃x ∈ A φ → ∃x ∈ A ψ)
Theorem	r19.22d 1276	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (x ∈ A → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	r19.22dv2 1277	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
⊢ (φ → ((x ∈ A ∧ ψ) → (x ∈ B ∧ χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ B χ))
Theorem	r19.22dv 1278	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
⊢ (φ → (x ∈ A → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	r19.22sdv 1279	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	r19.22dva 1280	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	r19.12 1281	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers.
⊢ (∃x ∈ A ∀y ∈ B φ → ∀y ∈ B ∃x ∈ A φ)
Theorem	r19.23v 1282	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers.
⊢ (∀x ∈ A (φ → ψ) ↔ (∃x ∈ A φ → ψ))
Theorem	r19.23ai 1283	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (ψ → ∀xψ)    &   ⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∃x ∈ A φ → ψ)
Theorem	r19.23aiv 1284	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∃x ∈ A φ → ψ)
Theorem	r19.23ad 1285	Deduction from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ∀xφ)    &   ⊢ (χ → ∀xχ)    &   ⊢ (φ → (x ∈ A → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → χ))
Theorem	r19.23adv 1286	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → (x ∈ A → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → χ))
Theorem	r19.23aivv 1287	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ ((x ∈ A ∧ y ∈ B) → (φ → ψ))    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ → ψ)
Theorem	r19.23advv 1288	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
⊢ (φ → ((x ∈ A ∧ y ∈ B) → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ → χ))
Theorem	r19.26 1289	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers.
⊢ (∀x ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀x ∈ A ψ))
Theorem	r19.26-2 1290	Theorem 19.26 of [Margaris] p. 90 with 2 restricted quantifiers.
⊢ (∀x ∈ A ∀y ∈ B (φ ∧ ψ) ↔ (∀x ∈ A ∀y ∈ B φ ∧ ∀x ∈ A ∀y ∈ B ψ))
Theorem	r19.26m 1291	Theorem 19.26 of [Margaris] p. 90 with mixed quantifiers.
⊢ (∀x((x ∈ A → φ) ∧ (x ∈ B → ψ)) ↔ (∀x ∈ A φ ∧ ∀x ∈ B ψ))
Theorem	r19.15 1292	Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification.
⊢ (∀x ∈ A (φ ↔ ψ) → (∀x ∈ A φ ↔ ∀x ∈ A ψ))
Theorem	r19.27av 1293	Restricted version of one direction of Theorem 19.27 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
⊢ ((∀x ∈ A φ ∧ ψ) → ∀x ∈ A (φ ∧ ψ))
Theorem	r19.28av 1294	Restricted version of one direction of Theorem 19.28 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
⊢ ((φ ∧ ∀x ∈ A ψ) → ∀x ∈ A (φ ∧ ψ))
Theorem	r19.29 1295	Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers.
⊢ ((∀x ∈ A φ ∧ ∃x ∈ A ψ) → ∃x ∈ A (φ ∧ ψ))
Theorem	r19.29r 1296	Variation of Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers.
⊢ ((∃x ∈ A φ ∧ ∀x ∈ A ψ) → ∃x ∈ A (φ ∧ ψ))
Theorem	r19.32v 1297	Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers.
⊢ (∀x ∈ A (φ ∨ ψ) ↔ (φ ∨ ∀x ∈ A ψ))
Theorem	r19.35 1298	Restricted quantifier version of Theorem 19.35 of [Margaris] p. 90.
⊢ (∃x ∈ A (φ → ψ) ↔ (∀x ∈ A φ → ∃x ∈ A ψ))
Theorem	r19.36av 1299	One direction of a restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. The other direction doesn't hold when A is empty.
⊢ (∃x ∈ A (φ → ψ) → (∀x ∈ A φ → ψ))
Theorem	r19.37av 1300	Restricted version of one direction of Theorem 19.37 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
⊢ (∃x ∈ A (φ → ψ) → (φ → ∃x ∈ A ψ))