Description: Restricted quantifier version of 19.41 . See r19.41v for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010)
Ref | Expression | ||
---|---|---|---|
Hypothesis | r19.41.1 | ||
Assertion | r19.41 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.41.1 | ||
2 | anass | ||
3 | 2 | exbii | |
4 | 1 | 19.41 | |
5 | 3 4 | bitr3i | |
6 | df-rex | ||
7 | df-rex | ||
8 | 7 | anbi1i | |
9 | 5 6 8 | 3bitr4i |