Description: A weak version of wfr2 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020) (Proof shortened by Scott Fenton, 18-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wfrfun.1 | |
|
Assertion | wfr2a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wfrfun.1 | |
|
2 | wefr | |
|
3 | 2 | adantr | |
4 | weso | |
|
5 | sopo | |
|
6 | 4 5 | syl | |
7 | 6 | adantr | |
8 | simpr | |
|
9 | 3 7 8 | 3jca | |
10 | df-wrecs | |
|
11 | 1 10 | eqtri | |
12 | 11 | fpr2a | |
13 | 9 12 | sylan | |
14 | simpr | |
|
15 | 1 | wfrresex | |
16 | 14 15 | opco2 | |
17 | 13 16 | eqtrd | |