P. 385 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38401-38500   *Has distinct variable group(s)

Type	Label	Description
Statement
21.25.3  Equality deductions A collection of theorems for commuting equalities (or biconditionals) with other constructs.
Theorem	iuneq2f 38401	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	rabeq12f 38402	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	csbeq12 38403	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 𝐶 = 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐷)
Theorem	sbeqi 38404	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ ((𝑥 = 𝑦 ∧ ∀𝑧(𝜑 ↔ 𝜓)) → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜓))
Theorem	ralbi12f 38405	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓)) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	oprabbi 38406	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	mpobi123f 38407*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	iuneq12f 38408	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iineq12f 38409	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐷) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	opabbi 38410	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	mptbi12f 38411	Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐷 = 𝐸) → (𝑥 ∈ 𝐴 ↦ 𝐷) = (𝑥 ∈ 𝐵 ↦ 𝐸))
21.25.4  Miscellanea Work in progress or things that do not belong anywhere else.
Theorem	orcomdd 38412	Commutativity of logic disjunction, in double deduction form. Should not be moved to main, see PR #3034 in Github. Use orcomd 872 instead. (Contributed by Giovanni Mascellani, 19-Mar-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∨ 𝜒)))
Theorem	scottexf 38413*	A version of scottex 9809 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V
Theorem	scott0f 38414*	A version of scott0 9810 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅)
Theorem	scottn0f 38415*	A version of scott0f 38414 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅)
Theorem	ac6s3f 38416*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 38417*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
Theorem	ac6s6f 38418*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
21.26  Mathbox for Peter Mazsa
21.26.1  Notations
Syntax	cxrn 38419	Extend the definition of a class to include the range Cartesian product class.
class (𝐴 ⋉ 𝐵)
Syntax	cqmap 38420	Extend the definition of a class to include the quotient map of a class.
class QMap 𝑅
Syntax	cadjliftmap 38421	Extend the definition of a class to include the class of adjoined lift maps.
class (𝑅 AdjLiftMap 𝐴)
Syntax	cblockliftmap 38422	Extend the definition of a class to include the class of block lift maps.
class (𝑅 BlockLiftMap 𝐴)
Syntax	csucmap 38423	Extend the definition of a class to include the class of successor maps.
class SucMap
Syntax	csuccl 38424	Extend the definition of a class to include the class of successors.
class Suc
Syntax	cpre 38425	Extend the definition of a class to include the predecessor of a class.
class pre 𝑁
Syntax	cblockliftfix 38426	Extend the definition of a class to include the class of equilibrium block lifts.
class BlockLiftFix
Syntax	cshiftstable 38427	Extend the definition of a class to include the shift stability class.
class (𝑆 ShiftStable 𝐹)
Syntax	ccoss 38428	Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.)
class ≀ 𝑅
Syntax	ccoels 38429	Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.)
class ∼ 𝐴
Syntax	crels 38430	Extend the definition of a class to include the relation class.
class Rels
Syntax	cssr 38431	Extend the definition of a class to include the subset class.
class S
Syntax	crefs 38432	Extend the definition of a class to include the reflexivity class.
class Refs
Syntax	crefrels 38433	Extend the definition of a class to include the reflexive relations class.
class RefRels
Syntax	wrefrel 38434	Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.)
wff RefRel 𝑅
Syntax	ccnvrefs 38435	Extend the definition of a class to include the converse reflexivity class.
class CnvRefs
Syntax	ccnvrefrels 38436	Extend the definition of a class to include the converse reflexive relations class.
class CnvRefRels
Syntax	wcnvrefrel 38437	Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.)
wff CnvRefRel 𝑅
Syntax	csyms 38438	Extend the definition of a class to include the symmetry class.
class Syms
Syntax	csymrels 38439	Extend the definition of a class to include the symmetry relations class.
class SymRels
Syntax	wsymrel 38440	Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.)
wff SymRel 𝑅
Syntax	ctrs 38441	Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5208).
class Trs
Syntax	ctrrels 38442	Extend the definition of a class to include the transitive relations class.
class TrRels
Syntax	wtrrel 38443	Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.)
wff TrRel 𝑅
Syntax	ceqvrels 38444	Extend the definition of a class to include the equivalence relations class.
class EqvRels
Syntax	weqvrel 38445	Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.)
wff EqvRel 𝑅
Syntax	ccoeleqvrels 38446	Extend the definition of a class to include the coelement equivalence relations class.
class CoElEqvRels
Syntax	wcoeleqvrel 38447	Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.)
wff CoElEqvRel 𝐴
Syntax	credunds 38448	Extend the definition of a class to include the redundancy class.
class Redunds
Syntax	wredund 38449	Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.)
wff 𝐴 Redund ⟨𝐵, 𝐶⟩
Syntax	wredundp 38450	Extend wff definition to include the redundancy operator for propositions.
wff redund (𝜑, 𝜓, 𝜒)
Syntax	cdmqss 38451	Extend the definition of a class to include the domain quotients class.
class DomainQss
Syntax	wdmqs 38452	Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.)
wff 𝑅 DomainQs 𝐴
Syntax	cers 38453	Extend the definition of a class to include the equivalence relations on their domain quotients class.
class Ers
Syntax	werALTV 38454	Extend the definition of a wff to include the equivalence relation on its domain quotient predicate. (Read: 𝑅 is an equivalence relation on its domain quotient 𝐴.)
wff 𝑅 ErALTV 𝐴
Syntax	cpeters 38455	Extend the definition of a class to include the blocklift-stable equivalence relations class.
class PetErs
Syntax	cpet2ers 38456	Extend the definition of a class to include the grade- and blocklift-stable equivalence relations class.
class Pet2Ers
Syntax	ccomembers 38457	Extend the definition of a class to include the comember equivalence relations class.
class CoMembErs
Syntax	wcomember 38458	Extend the definition of a wff to include the comember equivalence relation predicate. (Read: the comember equivalence relation on 𝐴, or, the restricted coelement equivalence relation on its domain quotient 𝐴.)
wff CoMembEr 𝐴
Syntax	cfunss 38459	Extend the definition of a class to include the function set class.
class Funss
Syntax	cfunsALTV 38460	Extend the definition of a class to include the functions class, i.e., the function relations class.
class FunsALTV
Syntax	wfunALTV 38461	Extend the definition of a wff to include the function predicate, i.e., the function relation predicate. (Read: 𝐹 is a function.)
wff FunALTV 𝐹
Syntax	cdisjss 38462	Extend the definition of a class to include the disjoint set class.
class Disjss
Syntax	cdisjs 38463	Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class.
class Disjs
Syntax	wdisjALTV 38464	Extend the definition of a wff to include the disjoint predicate, i.e., the disjoint relation predicate. (Read: 𝑅 is a disjoint.)
wff Disj 𝑅
Syntax	celdisjs 38465	Extend the definition of a class to include the disjoint elements class, i.e., the disjoint element relations class.
class ElDisjs
Syntax	weldisj 38466	Extend the definition of a wff to include the disjoint element predicate, i.e., the disjoint element relation predicate. (Read: the elements of 𝐴 are disjoint.)
wff ElDisj 𝐴
Syntax	wantisymrel 38467	Extend the definition of a wff to include the antisymmetry relation predicate. (Read: 𝑅 is an antisymmetric relation.)
wff AntisymRel 𝑅
Syntax	cparts 38468	Extend the definition of a class to include the partitions class, i.e., the partition relations class.
class Parts
Syntax	wpart 38469	Extend the definition of a wff to include the partition predicate, i.e., the partition relation predicate. (Read: 𝐴 is a partition by 𝑅.)
wff 𝑅 Part 𝐴
Syntax	cmembparts 38470	Extend the definition of a class to include the member partitions class, i.e., the member partition relations class.
class MembParts
Syntax	wmembpart 38471	Extend the definition of a wff to include the member partition predicate, i.e., the member partition relation predicate. (Read: 𝐴 is a member partition.)
wff MembPart 𝐴
Syntax	cpetparts 38472	Extend the definition of a class to include the blocklift-stable partitions class.
class PetParts
Syntax	cpet2parts 38473	Extend the definition of a class to include the grade- and blocklift-stable partitions class.
class Pet2Parts
21.26.2  Preparatory theorems
Theorem	el2v1 38474	New way (elv 3447, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	el3v1 38475	New way (elv 3447, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	el3v2 38476	New way (elv 3447, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	el3v12 38477	New way (elv 3447, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	el3v13 38478	New way (elv 3447, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	el3v23 38479	New way (elv 3447, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	anan 38480	Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏))))
Theorem	triantru3 38481	A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	biorfd 38482	A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∨ 𝜒)))
Theorem	eqbrtr 38483	Substitution of equal classes in binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	eqbrb 38484	Substitution of equal classes in a binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴𝑅𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵𝑅𝐶))
Theorem	eqeltr 38485	Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	eqelb 38486	Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 17-Jul-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶))
Theorem	eqeqan2d 38487	Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	disjresin 38488	The restriction to a disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝑅 ↾ (𝐴 ∩ 𝐵)) = ∅)
Theorem	disjresdisj 38489	The intersection of restrictions to disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∩ (𝑅 ↾ 𝐵)) = ∅)
Theorem	disjresdif 38490	The difference between restrictions to disjoint is the first restriction. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴))
Theorem	disjresundif 38491	Lemma for ressucdifsn2 38732. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ (𝐴 ∪ 𝐵)) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴))
Theorem	inres2 38492	Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴)
Theorem	coideq 38493	Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵))
Theorem	nexmo1 38494	If there is no case where wff is true, it is true for at most one case. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑)
Theorem	eqab2 38495	Implication of a class abstraction. (Contributed by Peter Mazsa, 16-Apr-2019.)
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	r2alan 38496*	Double restricted universal quantification, special case. (Contributed by Peter Mazsa, 17-Jun-2020.)
⊢ (∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓))
Theorem	ssrabi 38497	Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabimbieq 38498	Restricted equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	abeqin 38499*	Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑}
Theorem	abeqinbi 38500*	Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    &   ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓}