Theorem dfatopafv2b

Description: Equivalence of function value and ordered pair membership, analogous to fnopfvb or funopfvb . (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	dfatopafv2b	$$⊢\left(F\mathrm{defAt}A\wedge B\in W\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow ⟨A,B⟩\in F\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfatbrafv2b	$$⊢\left(F\mathrm{defAt}A\wedge B\in W\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow AFB\right)$$
2		df-br	$$⊢AFB\leftrightarrow ⟨A,B⟩\in F$$
3	1 2	bitrdi	$$⊢\left(F\mathrm{defAt}A\wedge B\in W\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow ⟨A,B⟩\in F\right)$$