| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssrab2 4080 | . . . . . 6
⊢ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} ⊆ 𝐴 | 
| 2 |  | sseqin2 4223 | . . . . . 6
⊢ ({𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} ⊆ 𝐴 ↔ (𝐴 ∩ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | 
| 3 | 1, 2 | mpbi 230 | . . . . 5
⊢ (𝐴 ∩ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} | 
| 4 |  | dfrab2 4320 | . . . . 5
⊢ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} = ({𝑦 ∣ 𝑦𝑅𝑋} ∩ 𝐴) | 
| 5 | 3, 4 | eqtr2i 2766 | . . . 4
⊢ ({𝑦 ∣ 𝑦𝑅𝑋} ∩ 𝐴) = (𝐴 ∩ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | 
| 6 |  | iniseg 6115 | . . . . . 6
⊢ (𝑋 ∈ V → (◡𝑅 “ {𝑋}) = {𝑦 ∣ 𝑦𝑅𝑋}) | 
| 7 | 6 | ineq2d 4220 | . . . . 5
⊢ (𝑋 ∈ V → (𝐴 ∩ (◡𝑅 “ {𝑋})) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋})) | 
| 8 |  | incom 4209 | . . . . 5
⊢ (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋}) = ({𝑦 ∣ 𝑦𝑅𝑋} ∩ 𝐴) | 
| 9 | 7, 8 | eqtrdi 2793 | . . . 4
⊢ (𝑋 ∈ V → (𝐴 ∩ (◡𝑅 “ {𝑋})) = ({𝑦 ∣ 𝑦𝑅𝑋} ∩ 𝐴)) | 
| 10 |  | iniseg 6115 | . . . . . 6
⊢ (𝑋 ∈ V → (◡(𝑅 ↾ 𝐴) “ {𝑋}) = {𝑦 ∣ 𝑦(𝑅 ↾ 𝐴)𝑋}) | 
| 11 |  | brres 6004 | . . . . . . . 8
⊢ (𝑋 ∈ V → (𝑦(𝑅 ↾ 𝐴)𝑋 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋))) | 
| 12 | 11 | abbidv 2808 | . . . . . . 7
⊢ (𝑋 ∈ V → {𝑦 ∣ 𝑦(𝑅 ↾ 𝐴)𝑋} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)}) | 
| 13 |  | df-rab 3437 | . . . . . . 7
⊢ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)} | 
| 14 | 12, 13 | eqtr4di 2795 | . . . . . 6
⊢ (𝑋 ∈ V → {𝑦 ∣ 𝑦(𝑅 ↾ 𝐴)𝑋} = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | 
| 15 | 10, 14 | eqtrd 2777 | . . . . 5
⊢ (𝑋 ∈ V → (◡(𝑅 ↾ 𝐴) “ {𝑋}) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | 
| 16 | 15 | ineq2d 4220 | . . . 4
⊢ (𝑋 ∈ V → (𝐴 ∩ (◡(𝑅 ↾ 𝐴) “ {𝑋})) = (𝐴 ∩ {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋})) | 
| 17 | 5, 9, 16 | 3eqtr4a 2803 | . . 3
⊢ (𝑋 ∈ V → (𝐴 ∩ (◡𝑅 “ {𝑋})) = (𝐴 ∩ (◡(𝑅 ↾ 𝐴) “ {𝑋}))) | 
| 18 |  | df-pred 6321 | . . 3
⊢
Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) | 
| 19 |  | df-pred 6321 | . . 3
⊢
Pred((𝑅 ↾
𝐴), 𝐴, 𝑋) = (𝐴 ∩ (◡(𝑅 ↾ 𝐴) “ {𝑋})) | 
| 20 | 17, 18, 19 | 3eqtr4g 2802 | . 2
⊢ (𝑋 ∈ V → Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋)) | 
| 21 |  | predprc 6359 | . . 3
⊢ (¬
𝑋 ∈ V →
Pred(𝑅, 𝐴, 𝑋) = ∅) | 
| 22 |  | predprc 6359 | . . 3
⊢ (¬
𝑋 ∈ V →
Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋) = ∅) | 
| 23 | 21, 22 | eqtr4d 2780 | . 2
⊢ (¬
𝑋 ∈ V →
Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋)) | 
| 24 | 20, 23 | pm2.61i 182 | 1
⊢
Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋) |