Theorem bnj115

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj115.1	|- ( et <-> A. n e. D ( ta -> th ) )
Assertion	bnj115	|- ( et <-> A. n ( ( n e. D /\ ta ) -> th ) )

Proof

Step	Hyp	Ref	Expression
1		bnj115.1	|- ( et <-> A. n e. D ( ta -> th ) )
2		df-ral	|- ( A. n e. D ( ta -> th ) <-> A. n ( n e. D -> ( ta -> th ) ) )
3		impexp	|- ( ( ( n e. D /\ ta ) -> th ) <-> ( n e. D -> ( ta -> th ) ) )
4	3	bicomi	|- ( ( n e. D -> ( ta -> th ) ) <-> ( ( n e. D /\ ta ) -> th ) )
5	4	albii	|- ( A. n ( n e. D -> ( ta -> th ) ) <-> A. n ( ( n e. D /\ ta ) -> th ) )
6	1 2 5	3bitri	|- ( et <-> A. n ( ( n e. D /\ ta ) -> th ) )