Metamath Proof Explorer


Theorem rabidd

Description: An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of Quine p. 16. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses rabidd.1 φ x A
rabidd.2 φ χ
Assertion rabidd φ x x A | χ

Proof

Step Hyp Ref Expression
1 rabidd.1 φ x A
2 rabidd.2 φ χ
3 rabid x x A | χ x A χ
4 1 2 3 sylanbrc φ x x A | χ